Commit 2025-07-06 01:51 8f8d0a6f

View on Github →

feat(Geometry/Euclidean/MongePoint) add theorems about orthocenter and circumcenter (#26781)

Estimated changes

Modified Mathlib/Geometry/Euclidean/MongePoint.lean

added theorem Affine.Simplex.smul_mongePoint_vsub_circumcenter_eq_sum_vsub

added theorem Affine.Triangle.dist_circumcenter_reflection_orthocenter

added theorem Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset

added theorem Affine.Triangle.orthocenter_vsub_circumcenter_eq_sum_vsub