mathlib

ccc98d0a - refactor(*): `midpoint`, `point_reflection`, and Mazur-Ulam in affine spaces (#4752)

refactor(*): `midpoint`, `point_reflection`, and Mazur-Ulam in affine spaces (#4752) * redefine `midpoint` for points in an affine space; * redefine `point_reflection` for affine spaces (as `equiv`, `affine_equiv`, and `isometric`); * define `const_vsub` as `equiv`, `affine_equiv`, and `isometric`; * define `affine_map.of_map_midpoint`; * fully migrate the proof of Mazur-Ulam theorem to affine spaces;