`BookProof.ChapterA3.chargeConj_mgamma_commutes` (μ : Fin 4) (v : Fin 4 → ℂ) : chargeConj (mgamma μ *ᵥ v) = mgamma μ *ᵥ chargeConj v

Initializing...

`BookProof.ChapterA3.chargeConj_mgamma_commutes` (μ : Fin 4) (v : Fin 4 → ℂ) : chargeConj (mgamma μ *ᵥ v) = mgamma μ *ᵥ chargeConj v · Prove2Me