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

Update ProdAssoc.lean

Browse source
This commit is contained in:
Pietro Monticone 2025-01-13 23:07:58 +01:00
parent 4eca44a404
commit dbc1a3e046
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/NodeIdentities/ProdAssoc.lean
View file

@ -21,7 +21,7 @@ namespace TensorTree
variable {S : TensorSpecies} {n n2 n3 : ℕ}
(c : Fin n → S.C) (c2 : Fin n2 → S.C) (c3 : Fin n3 → S.C)
/-- The permutation that arises from assocativity of `prod` node.
/-- The permutation that arises from associativity of `prod` node.
This permutation is defined using braiding and composition with `finSumFinEquiv`
based-isomorphisms. -/
def assocPerm : OverColor.mk