DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-11-07 15:48:43 +00:00
parent 27b9370c63
commit 9801d611b6
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/Tensors/Tree/Basic.lean
View file

@ -40,7 +40,7 @@ open MonoidalCategory
/-- The structure of a type of tensors e.g. Lorentz tensors, ordinary tensors
(vectors and matrices), complex Lorentz tensors. -/
structure TensorSpecies where
/-- The commutative ring over which we want to consider the tensors to live in,
/-- The commutative ring over which we want to consider the tensors to live in,
usually `ℝ` or `ℂ`. -/
k : Type
/-- An instance of `k` as a commutative ring. -/