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

Initializing...

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