mathlib

c0f16d26 - feat(analysis/normed_space/affine_isometry): new file, bundled affine isometries (#8660)

feat(analysis/normed_space/affine_isometry): new file, bundled affine isometries (#8660) This PR defines bundled affine isometries and affine isometry equivs, adapting the theory more or less wholesale from the linear isometry and affine map theories. In follow-up PRs I re-work the Mazur-Ulam and Euclidean geometry libraries to use these objects where appropriate.