Theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical

Modification history

2023-05-27 14:09
Mathlib/Geometry/Euclidean/Sphere/Power.lean
feat: port Geometry.Euclidean.Sphere.Power (#4418)
Added EuclideanGeometry.mul_dist_eq_mul_dist_of_cosphericalView on Github →