Theorem Submodule.orthogonalProjection_coe_eq_linearProjOfIsCompl

Modification history

2025-08-08 08:19

Mathlib/Analysis/InnerProductSpace/Projection.lean

chore(Analysis/InnerProductSpace/Projection): split file (#27851) …

Modified Submodule.orthogonalProjection_coe_eq_linearProjOfIsCompl View on Github →

2025-07-27 15:47

Mathlib/Analysis/InnerProductSpace/Projection.lean

feat(LinearAlgebra/Projection): lemmas on projections and invariant submodules (#25874) …

Added Submodule.orthogonalProjection_coe_eq_linearProjOfIsCompl View on Github →