Theorem Submodule.re_inner_orthogonalProjection_eq_normSq

Modification history

2025-07-15 08:11
Mathlib/Analysis/InnerProductSpace/Projection.lean
chore(Analysis/InnerProductSpace/Projection): deprecating `subtypeL ∘ orthogonalProjection` in favor of `starProjection` (#26877) …
Deleted Submodule.re_inner_orthogonalProjection_eq_normSqView on Github →
2025-05-31 23:10
Mathlib/Analysis/InnerProductSpace/Projection.lean
feat(Analysis/InnerProductSpace/Projection): add `Submodule.re_inner_orthogonalProjection_nonneg` (#24659)
Added Submodule.re_inner_orthogonalProjection_eq_normSqView on Github →