`BookProof.SmDiracSpinor.smFermiHam_zero_yukawa` (hD : Matrix (Fin 4) (Fin 4) ℂ) : smFermiHam hD (0 : Matrix (Fin 4) (Fin 4) ℂ) 0 = fermiBilin hD

Initializing...

`BookProof.SmDiracSpinor.smFermiHam_zero_yukawa` (hD : Matrix (Fin 4) (Fin 4) ℂ) : smFermiHam hD (0 : Matrix (Fin 4) (Fin 4) ℂ) 0 = fermiBilin hD · Prove2Me