Commit 2020-09-11 11:35 bc78621a

View on Github →

feat(geometry/euclidean/monge_point): reflection of circumcenter (#4062) Show that the distance from the orthocenter of a triangle to the reflection of the circumcenter in a side equals the circumradius (a key fact for proving various standard properties of orthocentric systems).

Estimated changes

Modified src/geometry/euclidean/circumcenter.lean

added theorem affine.simplex.reflection_circumcenter_eq_affine_combination_of_points_with_circumcenter

added def affine.simplex.reflection_circumcenter_weights_with_circumcenter

added theorem affine.simplex.sum_reflection_circumcenter_weights_with_circumcenter

Modified src/geometry/euclidean/monge_point.lean

added theorem affine.triangle.dist_orthocenter_reflection_circumcenter

added theorem affine.triangle.dist_orthocenter_reflection_circumcenter_finset