`BookProof.ChapterA3k.chir2_spinGenDiag_comm` (μ ν : Fin 4) : chir2 * spinGenDiag μ ν = spinGenDiag μ ν * chir2

Initializing...

`BookProof.ChapterA3k.chir2_spinGenDiag_comm` (μ ν : Fin 4) : chir2 * spinGenDiag μ ν = spinGenDiag μ ν * chir2 · Prove2Me