Congr results

Congr results

theorem TensorTree.perm_congr {S : TensorSpecies} {n m : ℕ} {c1 : Fin n → S.C} {c2 : Fin m → S.C} {T T' : TensorTree S c1} {σ σ' : IndexNotation.OverColor.mk c1 ⟶ IndexNotation.OverColor.mk c2} (h : σ = σ') (hT : T.tensor = T'.tensor) : (perm σ T).tensor = (perm σ' T').tensor

theorem TensorTree.perm_update {S : TensorSpecies} {n m : ℕ} {c1 : Fin n → S.C} {c2 : Fin m → S.C} {T : TensorTree S c1} {σ : IndexNotation.OverColor.mk c1 ⟶ IndexNotation.OverColor.mk c2} (σ' : IndexNotation.OverColor.mk c1 ⟶ IndexNotation.OverColor.mk c2) (h : σ = σ') : (perm σ T).tensor = (perm σ' T).tensor

theorem TensorTree.contr_congr {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} (i' : Fin n.succ.succ) {j : Fin n.succ} (j' : Fin n.succ) {h : c (i.succAbove j) = S.τ (c i)} {t : TensorTree S c} (hi : i = i' := by decide) (hj : j = j' := by decide) : (contr i j h t).tensor = (perm (IndexNotation.OverColor.mkIso ⋯).hom (contr i' j' ⋯ t)).tensor