Commit 2022-06-23 14:10 dd2e7add

feat(analysis/convex/strict_convex_space): isometries of strictly convex spaces are affine (#14837) Add the result that isometries of (affine spaces for) real normed spaces with strictly convex codomain are affine isometries. In particular, this applies to isometries of Euclidean spaces (we already have the instance that real inner product spaces are uniformly convex and thus strictly convex). Strict convexity means the surjectivity requirement of Mazur-Ulam can be avoided.