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.

Estimated changes

deleted theorem det_reflection
deleted theorem ker_orthogonalProjection
deleted theorem orthogonalProjectionFn_eq
deleted theorem orthogonalProjection_bot
deleted def reflection
deleted theorem reflection_apply
deleted theorem reflection_bot
deleted theorem reflection_eq_self_iff
deleted theorem reflection_inv
deleted theorem reflection_involutive
deleted theorem reflection_map
deleted theorem reflection_map_apply
deleted theorem reflection_mul_reflection
deleted theorem reflection_orthogonal
deleted theorem reflection_reflection
deleted theorem reflection_sub
deleted theorem reflection_symm