`BookProof.SmBrstGhost.matterGen_comm_ghostAnn` (m : ℕ) (T : Fin 12 → Matrix (Fin m) (Fin m) ℂ) (a b : Fin 12) : matterGen m T a * ghostAnn m b = ghostAnn m b * matterGen m T a

Initializing...

`BookProof.SmBrstGhost.matterGen_comm_ghostAnn` (m : ℕ) (T : Fin 12 → Matrix (Fin m) (Fin m) ℂ) (a b : Fin 12) : matterGen m T a * ghostAnn m b = ghostAnn m b * matterGen m T a · Prove2Me