`BookProof.ChapterA4g.SUtwo_mul_conjTranspose` {S : Matrix (Fin 2) (Fin 2) ℂ} (hS : S ∈ SUtwo) : S * Sᴴ = 1

Initializing...

`BookProof.ChapterA4g.SUtwo_mul_conjTranspose` {S : Matrix (Fin 2) (Fin 2) ℂ} (hS : S ∈ SUtwo) : S * Sᴴ = 1 · Prove2Me