`BookProof.ChapterPauliLorentz.hermMat_vecOfMat` {H : Matrix (Fin 2) (Fin 2) ℂ} (hH : Hᴴ = H) : hermMat (vecOfMat H) = H

Initializing...

`BookProof.ChapterPauliLorentz.hermMat_vecOfMat` {H : Matrix (Fin 2) (Fin 2) ℂ} (hH : Hᴴ = H) : hermMat (vecOfMat H) = H · Prove2Me