Commit 2025-07-30 22:15 c8bbf53a

View on Github →

feat(Analysis/InnerProductSpace/Adjoint): v in star projection range iff ‖T v‖ = ‖v‖ (#27619)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

added theorem isStarProjection_iff_eq_starProjection

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

added theorem Submodule.mem_iff_norm_starProjection