Commit 2026-01-21 00:52 058472fb

View on Github →

feat(Geometry/Euclidean/Altitude): map and restrict lemmas (#32021) Add lemmas about altitude, altitudeFoot and height for simplices mapped under an affine isometry or restricted to an affine subspace. Moves:

Submodule.map_orthogonal -> Submodule.map_orthogonal_equiv

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

modified theorem Submodule.map_orthogonal

added theorem Submodule.map_orthogonal_equiv

Modified Mathlib/Geometry/Euclidean/Altitude.lean

added theorem Affine.Simplex.altitudeFoot_map

added theorem Affine.Simplex.altitudeFoot_restrict

added theorem Affine.Simplex.altitude_map

added theorem Affine.Simplex.altitude_restrict_eq_comap_subtype

added theorem Affine.Simplex.height_map

added theorem Affine.Simplex.height_restrict

added theorem Affine.Simplex.map_altitude_restrict

Modified Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

added theorem AffineMap.map_vectorSpan

deleted theorem AffineMap.vectorSpan_image_eq_submodule_map