Theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero

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