`BookProof.ChapterGammaCommutant.gamma_commutant_eq_scalars` : {X : Matrix (Fin 4) (Fin 4) ℂ | ∀ μ, X * mgamma μ = mgamma μ * X} = {X | ∃ c : ℂ, X = c • (1 : Matrix (Fin 4) (Fin 4)

Proved

BookProof.ChapterGammaCommutant.gamma_commutant_eq_scalars

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGammaCommutant.

BookProof.ChapterGammaCommutant.gamma_commutant_eq_scalars : {X : Matrix (Fin 4) (Fin 4) ℂ | ∀ μ, X * mgamma μ = mgamma μ * X} = {X | ∃ c : ℂ, X = c • (1 : Matrix (Fin 4) (Fin 4) ℂ)}

Formalization note: Lean 4 identifier BookProof.ChapterGammaCommutant.gamma_commutant_eq_scalars.

Preamble

-- Generated from ChapterGammaCommutant.lean — theorem BookProof.ChapterGammaCommutant.gamma_commutant_eq_scalars
import Mathlib
import Definitions.Def_ChapterGammaCommutant
import Definitions.Def_ChapterA3
open BookProof.ChapterA3
open BookProof.ChapterGammaCommutant


open Matrix


open BookProof.ChapterA3

Formal statement

theorem BookProof.ChapterGammaCommutant.gamma_commutant_eq_scalars :
    {X : Matrix (Fin 4) (Fin 4) ℂ | ∀ μ, X * mgamma μ = mgamma μ * X}
      = {X | ∃ c : ℂ, X = c • (1 : Matrix (Fin 4) (Fin 4) ℂ)} := by sorry

View graph