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

Merge pull request #229 from HEPLean/IndexNotation

Browse source 
docs: Small changes to Index notation
This commit is contained in:
Joseph Tooby-Smith 2024-11-07 16:17:24 +00:00 • committed by GitHub
commit 1a8bc9bf61
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -37,10 +37,10 @@ open IndexNotation
open CategoryTheory
open MonoidalCategory
/-- The structure of a type of tensors e.g. Lorentz tensors, Einstien tensors,
complex Lorentz tensors. -/
/-- 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. -/