Theorem isStarProjection_starProjection

Modification history

2025-07-15 08:11

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

chore(Analysis/InnerProductSpace/Projection): deprecating `subtypeL ∘ orthogonalProjection` in favor of `starProjection` (#26877) …

Modified isStarProjection_starProjection View on Github →

2025-07-11 01:56

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

feat(Analysis/InnerProductSpace/Projection): define `Submodule.starProjection` (#25958) …

Added isStarProjection_starProjection View on Github →