Commit 2025-07-27 14:59 8ac39d01

View on Github →

chore(Analysis/InnerProductAlgebra/Projection): adding norm and other results for Submodule.starProjection (#27317) Analogue results for Submodule.starProjection.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

added theorem Submodule.IsOrtho.starProjection_comp_starProjection

added theorem Submodule.lipschitzWith_starProjection

added theorem Submodule.norm_sq_eq_add_norm_sq_starProjection

added theorem Submodule.norm_starProjection

added theorem Submodule.norm_starProjection_apply

added theorem Submodule.norm_starProjection_apply_le

deleted theorem Submodule.orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero

added theorem Submodule.orthogonalProjection_orthogonal_apply_eq_zero

added theorem Submodule.starProjection_apply_eq_zero_iff

added theorem Submodule.starProjection_comp_starProjection_eq_zero_iff

added theorem Submodule.starProjection_comp_starProjection_of_le

added theorem Submodule.starProjection_mem_subspace_eq_self

added theorem Submodule.starProjection_norm_le

added theorem Submodule.starProjection_orthogonalComplement_singleton_eq_zero

added theorem Submodule.starProjection_orthogonal_apply_eq_zero