`BookProof.ChapterA3.mgamma5_sq` : mgamma5 * mgamma5 = -(1 : Matrix (Fin 4) (Fin 4) ℂ)

Initializing...

`BookProof.ChapterA3.mgamma5_sq` : mgamma5 * mgamma5 = -(1 : Matrix (Fin 4) (Fin 4) ℂ) · Prove2Me