Theorem Affine.Simplex.smul_mongePoint_vsub_circumcenter_eq_sum_vsub

Modification history

2025-07-06 01:51

Mathlib/Geometry/Euclidean/MongePoint.lean

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

Added Affine.Simplex.smul_mongePoint_vsub_circumcenter_eq_sum_vsub View on Github →