`BookProof.ChapterPauliSU2.spinorAction_isHermitian` (T : Matrix (Fin 2) (Fin 2) ℂ) {X : Matrix (Fin 2) (Fin 2) ℂ} (hX : Xᴴ = X) : (spinorAction T X)ᴴ = spinorAction T X

Initializing...

`BookProof.ChapterPauliSU2.spinorAction_isHermitian` (T : Matrix (Fin 2) (Fin 2) ℂ) {X : Matrix (Fin 2) (Fin 2) ℂ} (hX : Xᴴ = X) : (spinorAction T X)ᴴ = spinorAction T X · Prove2Me