mathlib3

dd2e7add - feat(analysis/convex/strict_convex_space): isometries of strictly convex spaces are affine (#14837)

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. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>