`BookProof.ChapterA3.fixesNullAxis_iff_conj` (T : Matrix (Fin 2) (Fin 2) ℂ) : FixesNullAxis (Upsilon T) ↔ Tᴴ * (pauliσ 0 + pauliσ 3) * T = pauliσ 0 + pauliσ 3

Initializing...

`BookProof.ChapterA3.fixesNullAxis_iff_conj` (T : Matrix (Fin 2) (Fin 2) ℂ) : FixesNullAxis (Upsilon T) ↔ Tᴴ * (pauliσ 0 + pauliσ 3) * T = pauliσ 0 + pauliσ 3 · Prove2Me