Mathlib v3 is deprecated. Go to Mathlib v4

Theorem euclidean_geometry.mul_dist_le_mul_dist_add_mul_dist

Modification history

2022-06-18 16:59
src/geometry/euclidean/inversion.lean
feat(geometry/euclidean/inversion) new file (#14692) …
Added euclidean_geometry.mul_dist_le_mul_dist_add_mul_distView on Github →