`BookProof.SmBrstGhost.smBrstCharge_nilpotent` {m : ℕ} {T : Fin 12 → Matrix (Fin m) (Fin m) ℂ} {f3 : Fin 8 → Fin 8 → Fin 8 → ℝ} (hT : ClosesWithStructureConstants T (smStruct f3))

Initializing...

`BookProof.SmBrstGhost.smBrstCharge_nilpotent` {m : ℕ} {T : Fin 12 → Matrix (Fin m) (Fin m) ℂ} {f3 : Fin 8 → Fin 8 → Fin 8 → ℝ} (hT : ClosesWithStructureConstants T (smStruct f3)) · Prove2Me