Commit 2025-02-10 08:08 422990cf
View on Github →refactor(Geometry/Euclidean/Basic,Analysis/Normed/Affine/AddTorsor): generalize dist_left_midpoint_eq_dist_right_midpoint (#21617)
The lemma dist_left_midpoint_eq_dist_right_midpoint has an unnecessary restriction to inner product spaces, when the two lemmas dist_left_midpoint and dist_right_midpoint it uses are stated and proved more generally. Move it to
Mathlib.Analysis.Normed.Affine.AddTorsor and thus make the statement more general.