`BookProof.ChapterA3.nullConj_iff_form` (T : Matrix (Fin 2) (Fin 2) ℂ) : Tᴴ * (pauliσ 0 + pauliσ 3) * T = pauliσ 0 + pauliσ 3 ↔ T 0 1 = 0 ∧ Complex.normSq (T 0 0) = 1

Initializing...

`BookProof.ChapterA3.nullConj_iff_form` (T : Matrix (Fin 2) (Fin 2) ℂ) : Tᴴ * (pauliσ 0 + pauliσ 3) * T = pauliσ 0 + pauliσ 3 ↔ T 0 1 = 0 ∧ Complex.normSq (T 0 0) = 1 · Prove2Me