`BookProof.ChapterLorentzRealRep.conj_inv_10` : ∀ S ∈ Omega, ∀ i, S * b10 i * cinv S ∈ SB10

Initializing...

`BookProof.ChapterLorentzRealRep.conj_inv_10` : ∀ S ∈ Omega, ∀ i, S * b10 i * cinv S ∈ SB10 · Prove2Me