`BookProof.BookBrstYangMills.mom_comm_chi` (μ : Fin 4) (a b : Fin N) : mom (N := N) μ a * chiOp b = chiOp b * mom μ a

Initializing...

`BookProof.BookBrstYangMills.mom_comm_chi` (μ : Fin 4) (a b : Fin N) : mom (N := N) μ a * chiOp b = chiOp b * mom μ a · Prove2Me