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

refactor: Line lengths

Browse source
This commit is contained in:
jstoobysmith 2024-10-20 14:32:21 +00:00
parent 6ebd7a2137
commit a0d9d6766a
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/Tensors/Tree/NodeIdentities/PermProd.lean
View file

@ -26,12 +26,14 @@ variable {S : TensorStruct} {n n' n2 : ℕ}
/-- The permutation that arises when moving a `perm` node in the left entry through a `prod` node.
This permutation is defined using right-whiskering and composition with `finSumFinEquiv`
based-isomorphisms. -/
def permProdLeft := (equivToIso finSumFinEquiv).inv ≫ σ ▷ OverColor.mk c2 ≫ (equivToIso finSumFinEquiv).hom
def permProdLeft := (equivToIso finSumFinEquiv).inv ≫ σ ▷ OverColor.mk c2
≫ (equivToIso finSumFinEquiv).hom
/-- The permutation that arises when moving a `perm` node in the right entry through a `prod` node.
This permutation is defined using left-whiskering and composition with `finSumFinEquiv`
based-isomorphisms. -/
def permProdRight:= (equivToIso finSumFinEquiv).inv ≫ OverColor.mk c2 ◁ σ ≫ (equivToIso finSumFinEquiv).hom
def permProdRight := (equivToIso finSumFinEquiv).inv ≫ OverColor.mk c2 ◁ σ
≫ (equivToIso finSumFinEquiv).hom
/-- When a `prod` acts on a `perm` node in the left entry, the `perm` node can be moved through
the `prod` node via right-whiskering. -/