2025-07-27 14:59
Mathlib/Analysis/InnerProductSpace/Projection.lean
chore(Analysis/InnerProductAlgebra/Projection): adding norm and other results for `Submodule.starProjection` (#27317) …
Added Submodule.starProjection_comp_starProjection_eq_zero_iff