Mathlib v3 is deprecated. Go to Mathlib v4

Theorem isometry.coe_affine_isometry_of_strict_convex_space

Modification history

2022-06-23 14:10
src/analysis/convex/strict_convex_space.lean
feat(analysis/convex/strict_convex_space): isometries of strictly convex spaces are affine (#14837) …
Added isometry.coe_affine_isometry_of_strict_convex_spaceView on Github →