Commit 2025-05-18 15:44 ab52f0ab

View on Github →

chore: generalize from n + 1 to NeZero (#24988) This makes altitude consistent with altitudeFoot. I could also be persuaded that this is backwards and we should go the other way.

Estimated changes

Modified Mathlib/Geometry/Euclidean/Altitude.lean

modified theorem Affine.Simplex.affineSpan_pair_altitudeFoot_eq_altitude

modified theorem Affine.Simplex.affineSpan_pair_eq_altitude_iff

modified def Affine.Simplex.altitude

modified theorem Affine.Simplex.altitudeFoot_mem_altitude

modified theorem Affine.Simplex.altitude_def

modified theorem Affine.Simplex.direction_altitude

modified theorem Affine.Simplex.finrank_direction_altitude

modified theorem Affine.Simplex.mem_altitude

modified theorem Affine.Simplex.vectorSpan_isOrtho_altitude_direction