`BookProof.ChapterGammaCommutant.gamma_intertwiner_unique` (S T : Matrix (Fin 4) (Fin 4) ℂ) (hS : IsUnit S.det) (hSg : ∀ μ, S * mgamma μ = mgamma μ * S) (hTg : ∀ μ, T * mgamma μ =

Proved

BookProof.ChapterGammaCommutant.gamma_intertwiner_unique

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGammaCommutant.

BookProof.ChapterGammaCommutant.gamma_intertwiner_unique (S T : Matrix (Fin 4) (Fin 4) ℂ) (hS : IsUnit S.det) (hSg : ∀ μ, S * mgamma μ = mgamma μ * S) (hTg : ∀ μ, T * mgamma μ = mgamma μ * T) : ∃ c : ℂ, T = c • S

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

Preamble

-- Generated from ChapterGammaCommutant.lean — theorem BookProof.ChapterGammaCommutant.gamma_intertwiner_unique
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_intertwiner_unique (S T : Matrix (Fin 4) (Fin 4) ℂ) (hS : IsUnit S.det)
    (hSg : ∀ μ, S * mgamma μ = mgamma μ * S) (hTg : ∀ μ, T * mgamma μ = mgamma μ * T) :
    ∃ c : ℂ, T = c • S := by sorry

View graph