`BookProof.ChapterLorentzRealRepSum.span_bAllR_eq` : Submodule.span ℝ (Set.range bAllR) = WHalf ⊔ W10 ⊔ WPs

Initializing...

`BookProof.ChapterLorentzRealRepSum.span_bAllR_eq` : Submodule.span ℝ (Set.range bAllR) = WHalf ⊔ W10 ⊔ WPs · Prove2Me