Commit 2025-07-27 19:24 9d7b3506

View on Github →

chore(Analysis/InnerProductSpace/Projection): change _of_completeSpace to _of_hasOrthogonalProjection (#27559) This PR renames the results because they use Submodule.HasOrthogonalProjection and not CompleteSpace.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

deleted theorem Submodule.isCompl_orthogonal_of_completeSpace

added theorem Submodule.isCompl_orthogonal_of_hasOrthogonalProjection

deleted theorem Submodule.sup_orthogonal_inf_of_completeSpace

added theorem Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection

deleted theorem Submodule.sup_orthogonal_of_completeSpace

added theorem Submodule.sup_orthogonal_of_hasOrthogonalProjection

Modified Mathlib/Analysis/InnerProductSpace/Semisimple.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Geometry/Euclidean/Inversion/Calculus.lean

Modified Mathlib/Geometry/Euclidean/Projection.lean