Commit 2025-05-01 14:04 22a178a0

refactor(Geometry/Euclidean): split out altitudes (#24504) Move the definition of Affine.Simplex.altitude and associated API from MongePoint.lean to a separate file, in preparation for setting up other associated definitions (as discussed in #23752) that are of use without involving the Monge point / orthocenter. There are no changes to definitions, statements or proofs; this is just moving content from one file to another.