mathlib

e3968f66 - feat(linear_algebra/affine_space/midpoint): `midpoint_vsub`, `vsub_midpoint` (#17278)

feat(linear_algebra/affine_space/midpoint): `midpoint_vsub`, `vsub_midpoint` (#17278) Add lemmas about subtracting an arbitrary point from a midpoint (or vice versa), in relation to subtractions involving the endpoints.