`BookProof.ChapterA3.mgammaZ_clifford` (μ ν : Fin 4) : mgammaZ μ * mgammaZ ν + mgammaZ ν * mgammaZ μ = (-2 * minkowskiZ μ ν) • (1 : Matrix (Fin 4) (Fin 4) ℤ)

Initializing...

`BookProof.ChapterA3.mgammaZ_clifford` (μ ν : Fin 4) : mgammaZ μ * mgammaZ ν + mgammaZ ν * mgammaZ μ = (-2 * minkowskiZ μ ν) • (1 : Matrix (Fin 4) (Fin 4) ℤ) · Prove2Me