Mathlib v3 is deprecated. Go to Mathlib v4

Theorem euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical

Modification history

2023-03-16 11:15
src/geometry/euclidean/sphere/power.lean
refactor(geometry/euclidean): split out spheres (#18220) …
Modified euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cosphericalView on Github →
2021-06-21 19:43
src/geometry/euclidean/sphere.lean
feat(geometry/euclidean/sphere): proof of Freek thm 95 - Ptolemy’s Theorem (#7329)
Added euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cosphericalView on Github →