`BookProof.ChapterA3.pauliCoeff_one` (μ : Fin 4) : pauliCoeff (1 : Matrix (Fin 2) (Fin 2) ℂ) μ = if μ = 0 then 1 else 0

Initializing...

`BookProof.ChapterA3.pauliCoeff_one` (μ : Fin 4) : pauliCoeff (1 : Matrix (Fin 2) (Fin 2) ℂ) μ = if μ = 0 then 1 else 0 · Prove2Me