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
Submodule
namespace.