Theorem dist_left_midpoint_eq_dist_right_midpoint

Modification history

2025-02-10 08:08
Mathlib/Analysis/Normed/Affine/AddTorsor.lean
refactor(Geometry/Euclidean/Basic,Analysis/Normed/Affine/AddTorsor): generalize `dist_left_midpoint_eq_dist_right_midpoint` (#21617) …
Added dist_left_midpoint_eq_dist_right_midpointView on Github →