`BookProof.ChapterParityHiggs.higgs_real_structure` (v : Fin 2 × Fin 2 → ℂ) : realityOp higgsReal (realityOp higgsReal v) = v

Initializing...

`BookProof.ChapterParityHiggs.higgs_real_structure` (v : Fin 2 × Fin 2 → ℂ) : realityOp higgsReal (realityOp higgsReal v) = v · Prove2Me