`BookProof.ChapterCPTHamiltonian.kinSum_MassA_anticomm` (k : Fin 3 → ℝ) : (∑ j : Fin 3, (k j : ℂ) • Kin j) * MassA + MassA * (∑ j : Fin 3, (k j : ℂ) • Kin j) = 0

Initializing...

`BookProof.ChapterCPTHamiltonian.kinSum_MassA_anticomm` (k : Fin 3 → ℝ) : (∑ j : Fin 3, (k j : ℂ) • Kin j) * MassA + MassA * (∑ j : Fin 3, (k j : ℂ) • Kin j) = 0 · Prove2Me