mathlib

9e4ef854 - feat(linear_algebra/affine_space): define `affine_equiv.mk'` (#4750)

feat(linear_algebra/affine_space): define `affine_equiv.mk'` (#4750) Similarly to `affine_map.mk'`, this constructor checks that the map agrees with its linear part only for one base point.