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

refactor: Spelling

Browse source
This commit is contained in:
jstoobysmith 2024-11-06 11:41:59 +00:00
parent 5acf22c479
commit 5272ed1607
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,7 +37,7 @@ open IndexNotation
open CategoryTheory
open MonoidalCategory
/-- The sturcture of a type of tensors e.g. Lorentz tensors, Einstien tensors,
/-- The structure of a type of tensors e.g. Lorentz tensors, Einstien tensors,
complex Lorentz tensors. -/
structure TensorSpecies where
/-- The commutative ring over which we want to consider the tensors to live in,
@ -555,13 +555,13 @@ end TensorSpecies
inductive TensorTree (S : TensorSpecies) : {n : ℕ} → (Fin n → S.C) → Type where
/-- A general tensor node. -/
| tensorNode {n : ℕ} {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : TensorTree S c
/-- A node correpsonding to the scalar multiple of a tensor by a element of the field. -/
/-- A node corresponding to the scalar multiple of a tensor by a element of the field. -/
| smul {n : ℕ} {c : Fin n → S.C} : S.k → TensorTree S c → TensorTree S c
/-- A node corresponding to negation of a tensor. -/
| neg {n : ℕ} {c : Fin n → S.C} : TensorTree S c → TensorTree S c
/-- A node corresponding to the addition of two tensors. -/
| add {n : ℕ} {c : Fin n → S.C} : TensorTree S c → TensorTree S c → TensorTree S c
/-- A node correpsonding to the action of a group element on a tensor. -/
/-- A node corresponding to the action of a group element on a tensor. -/
| action {n : ℕ} {c : Fin n → S.C} : S.G → TensorTree S c → TensorTree S c
/-- A node corresponding to the permutation of indices of a tensor. -/
| perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}