`BookProof.ChapterA3.dgamma_commutant_scalar` (M : Matrix (Fin 4) (Fin 4) ℂ) (h : ∀ μ, M * dgamma μ = dgamma μ * M) : M = M 0 0 • (1 : Matrix (Fin 4) (Fin 4) ℂ)

Initializing...

`BookProof.ChapterA3.dgamma_commutant_scalar` (M : Matrix (Fin 4) (Fin 4) ℂ) (h : ∀ μ, M * dgamma μ = dgamma μ * M) : M = M 0 0 • (1 : Matrix (Fin 4) (Fin 4) ℂ) · Prove2Me