Commit 2025-05-01 21:43 baa6a159

feat(Geometry/Euclidean/Altitude): altitudeFoot, height (#24525) As discussed in #23752, add definitions for the foot of an altitude of a simplex and the height of a vertex of a simplex. Provide a minimal linkage to the definition of altitude (for example, altitudeFoot lies in the altitude). No change is made to the definition or existing API for altitude. (In particular, that definition uses an older style of {n : ℕ} (s : Simplex ℝ P (n + 1)) where faceOpposite and altitudeFoot use the newer approach of {n : ℕ} [NeZero n] (s : Simplex ℝ P n).) The existing lemmas ne_orthogonalProjection_faceOpposite and dist_orthogonalProjection_faceOpposite_pos are changed to be about altitudeFoot and height, renamed and moved. I think they are recent enough that no deprecations are needed.