`BookProof.ChapterElectroweakFieldStrength.linear_trace` (G : Fin 3 → ℂ) (j : Fin 3) : ((∑ m, G m • ((1 / 2 : ℂ) • pauliV m)) * pauliV j).trace = G j

Initializing...

`BookProof.ChapterElectroweakFieldStrength.linear_trace` (G : Fin 3 → ℂ) (j : Fin 3) : ((∑ m, G m • ((1 / 2 : ℂ) • pauliV m)) * pauliV j).trace = G j · Prove2Me