`BookProof.ChapterA3.mgamma_conjTranspose` (μ : Fin 4) : (mgamma μ)ᴴ = (if μ = 0 then (-1 : ℂ) else 1) • mgamma μ

Initializing...

`BookProof.ChapterA3.mgamma_conjTranspose` (μ : Fin 4) : (mgamma μ)ᴴ = (if μ = 0 then (-1 : ℂ) else 1) • mgamma μ · Prove2Me