`BookProof.ChapterLorentzRealRep.conj_inv_half` : ∀ S ∈ Omega, ∀ i, S * bHalf i * cinv S ∈ SBHalf

Initializing...

`BookProof.ChapterLorentzRealRep.conj_inv_half` : ∀ S ∈ Omega, ∀ i, S * bHalf i * cinv S ∈ SBHalf · Prove2Me