Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-28 14:08 8461a7d3

View on Github →

feat(geometry/euclidean/monge_point): lemmas on altitudes and orthocenter (#4179) Add more lemmas about altitudes of a simplex and the orthocenter of a triangle. Some of these are just building out basic API that's mathematically trivial (e.g. showing that the altitude as defined is a one-dimensional affine subspace and providing an explicit form of its direction), while the results on the orthocenter have some geometrical content that's part of the preparation for defining and proving basic properties of orthocentric systems.

Estimated changes