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

[hrmacbeth]

Add constructions add_equiv.base_at (of type perm), linear_equiv.base_at (of type affine_equiv), and linear_isometry_equiv.base_at (of type affine_isometry_equiv), to describe the automorphism of an add_torsor/normed_add_torsor obtained by fixing a basepoint, temporarily identifying the add_torsor with its model space using this basepoint, and applying the add_equiv/linear_equiv/linear_isometry_equiv to the space under this identification.

Also API for these constructions and a few more missing lemmas.

---