`BookProof.ChapterPauliSU2.spinorAction_trace_of_unitary` {T : Matrix (Fin 2) (Fin 2) ℂ} (hT : Tᴴ * T = 1) (X : Matrix (Fin 2) (Fin 2) ℂ) : (spinorAction T X).trace = X.trace

Initializing...

`BookProof.ChapterPauliSU2.spinorAction_trace_of_unitary` {T : Matrix (Fin 2) (Fin 2) ℂ} (hT : Tᴴ * T = 1) (X : Matrix (Fin 2) (Fin 2) ℂ) : (spinorAction T X).trace = X.trace · Prove2Me