mathlib3

feat(algebra/add_torsor, linear_algebra/affine_space/affine_equiv, analysis/normed_space/affine_isometry): `base_at` construction

#8837

Open