Commit 2023-05-27 14:09 c7a9e113

View on Github →

feat: port Geometry.Euclidean.Sphere.Power (#4418)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Euclidean/Sphere/Power.lean

added theorem EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist

added theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical

added theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi

added theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero

added theorem InnerProductGeometry.mul_norm_eq_abs_sub_sq_norm