Commit 2025-04-22 07:21 c6bd6355
View on Github →chore: rename orthogonalProjection to Submodule.orthogonalProjection (#24247)
This PR puts orthogonalProjection, HasOrthogonalProjection and reflection in the Submodule namespace. This allows us to use dot-notation with these definitions. It also removes the name ambiguity with EuclideanGeometry.orthogonalProjection and EuclideanGeometry.reflection. Those can be moved to the AffineSubspace namespace in a future PR.
As discussed here: #lean4 > overloaded names can slow down elaboration
Moves:
- orthogonalProjection -> Submodule.orthogonalProjection
- HasOrthogonalProjection -> Submodule.HasOrthogonalProjection
- reflection -> Submodule.reflection
The definitions and many lemmas related to these have also been moved into the
Submodulenamespace.