Commit 2025-12-31 17:34 350ded7f

View on Github →

chore(Analysis/InnerProductSpace/Projection/Submodule): rename lemmas (#33337)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean

added theorem Submodule.orthogonalProjection_apply_eq_linearProjOfIsCompl

deleted theorem Submodule.orthogonalProjection_coe_eq_linearProjOfIsCompl

deleted theorem Submodule.orthogonalProjection_eq_linearProjOfIsCompl

deleted theorem Submodule.starProjection_coe_eq_isCompl_projection

added theorem Submodule.toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl

added theorem Submodule.toLinearMap_starProjection_eq_isComplProjection