`BookProof.ChapterLorentzRealRepFull.span_bFullR_eq` : Submodule.span ℝ (Set.range bFullR) = WHalf ⊔ W10 ⊔ WPs ⊔ WTwo

Initializing...

`BookProof.ChapterLorentzRealRepFull.span_bFullR_eq` : Submodule.span ℝ (Set.range bFullR) = WHalf ⊔ W10 ⊔ WPs ⊔ WTwo · Prove2Me