`BookProof.ChapterA3.mgamma_conjugation_unique_up_to_scalar` {S T : Matrix (Fin 4) (Fin 4) ℂ} (hS : IsUnit S.det) (hT : IsUnit T.det) (h : ∀ μ, S * mgamma μ * S⁻¹ = T * mgamma μ *

Initializing...

`BookProof.ChapterA3.mgamma_conjugation_unique_up_to_scalar` {S T : Matrix (Fin 4) (Fin 4) ℂ} (hS : IsUnit S.det) (hT : IsUnit T.det) (h : ∀ μ, S * mgamma μ * S⁻¹ = T * mgamma μ * · Prove2Me