mathlib3

35da8bde - feat(geometry/euclidean/angle/oriented/affine): equidistant points and `π / 2` rotations (#17722)

feat(geometry/euclidean/angle/oriented/affine): equidistant points and `π / 2` rotations (#17722) Add the following lemma: two different points are equidistant from a third point if and only if that third point equals some multiple of a `π / 2` rotation of the vector between those points, plus the midpoint of those points. In particular, this is useful for bisecting an isosceles triangle then applying trigonometric lemmas about right-angled triangles from #17683 to the result.