Update PermContr.lean

HEPLean · Jan 13, 2025 · 4eca44a · 4eca44a
1 parent af72d87
commit 4eca44a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
@@ -245,7 +245,7 @@ namespace TensorTree
 variable {S : TensorSpecies}
 
 /-- Permuting indices, and then contracting is equivalent to contracting and then permuting,
-  once care is taking about ensuring one is contracting the same idices. -/
+  once care is taking about ensuring one is contracting the same indices. -/
 lemma perm_contr {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C}
     {i : Fin n.succ.succ} {j : Fin n.succ}
     {h : c1 (i.succAbove j) = S.τ (c1 i)} (t : TensorTree S c)