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.
leanprover-community · Aug 18, 2021 · c0f16d2 · c0f16d2
1 parent d1b34f7
commit c0f16d2
Show file tree

Hide file tree

Showing 4 changed files with 465 additions and 15 deletions.
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
@@ -255,8 +255,8 @@ Affine and Euclidean Geometry:
     convex hull of a subset of an affine real space: 'convex_hull'
     extreme point: 'set.extreme_points'
   Euclidean affine spaces:
-    isometries of a Euclidean affine space:
-    group of isometries of a Euclidean affine space:
+    isometries of a Euclidean affine space: 'affine_isometry_equiv'
+    group of isometries of a Euclidean affine space: 'affine_isometry_equiv.group'
     isometries that do and do not preserve orientation:
     direct and opposite similarities of the plane:
     classification of isometries in two and three dimensions: