`BookProof.ChapterLorentzRealRep.conj_inv_ps` : ∀ S ∈ Omega, ∀ i, S * bPs i * cinv S ∈ SBPs

Initializing...

`BookProof.ChapterLorentzRealRep.conj_inv_ps` : ∀ S ∈ Omega, ∀ i, S * bPs i * cinv S ∈ SBPs · Prove2Me