`BookProof.ChapterMajoranaProp74.g_mul_A` {g ns : Matrix (Fin 4) (Fin 4) ℂ} (hg2 : g * g = 1) (hgns : g * ns = -(ns * g)) : g * (ns * g) = -ns

Initializing...

`BookProof.ChapterMajoranaProp74.g_mul_A` {g ns : Matrix (Fin 4) (Fin 4) ℂ} (hg2 : g * g = 1) (hgns : g * ns = -(ns * g)) : g * (ns * g) = -ns · Prove2Me