Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eq_line_map_of_dist_eq_mul_of_dist_eq_mul

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 eq_line_map_of_dist_eq_mul_of_dist_eq_mulView on Github →