`BookProof.ChapterMajoranaProp74.ns_mul_A` {g ns : Matrix (Fin 4) (Fin 4) ℂ} (hns2 : ns * ns = -1) : ns * (ns * g) = -g

Initializing...

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