`BookProof.ChapterElectroweakFieldStrength.electroweak_fieldStrength` (g : ℂ) (hg : g ≠ 0) (G Wμ Wν : Fin 3 → ℂ) (j : Fin 3) : proj g (Fmat g G Wμ Wν) j = G j

Initializing...

`BookProof.ChapterElectroweakFieldStrength.electroweak_fieldStrength` (g : ℂ) (hg : g ≠ 0) (G Wμ Wν : Fin 3 → ℂ) (j : Fin 3) : proj g (Fmat g G Wμ Wν) j = G j - g * ∑ k, ∑ l, eps j · Prove2Me