Lemmas related to complex Lorentz tensors.

theorem complexLorentzTensor.antiSymm_contr_symm {A : ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ![Color.up, Color.up])).V} {S : ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ![Color.down, Color.down])).V} (hA : (TensorTree.tensorNode A).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode A).neg).tensor) (hs : (TensorTree.tensorNode S).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode S)).tensor) : (TensorTree.contr 0 0 ⋯ (TensorTree.contr 0 1 ⋯ ((TensorTree.tensorNode A).prod (TensorTree.tensorNode S)))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![] ![] ⋯ ⋯) ⋯) (TensorTree.contr 0 0 ⋯ (TensorTree.contr 0 1 ⋯ ((TensorTree.tensorNode A).prod (TensorTree.tensorNode S)))).neg).tensor