Commit 2021-08-18 12:08 c0f16d26

View on Github →

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.

Estimated changes

added theorem affine_isometry.coe_id
added theorem affine_isometry.ext
added theorem affine_isometry.map_ne
added structure affine_isometry
added structure affine_isometry_equiv