`BookProof.ChapterGammaCommutant.gamma_commutant_scalar` (X : Matrix (Fin 4) (Fin 4) ℂ) (h : ∀ μ, X * mgamma μ = mgamma μ * X) : X = X 0 0 • (1 : Matrix (Fin 4) (Fin 4) ℂ)

Initializing...

`BookProof.ChapterGammaCommutant.gamma_commutant_scalar` (X : Matrix (Fin 4) (Fin 4) ℂ) (h : ∀ μ, X * mgamma μ = mgamma μ * X) : X = X 0 0 • (1 : Matrix (Fin 4) (Fin 4) ℂ) · Prove2Me