Theorem EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist

Modification history

2025-09-21 21:23
Mathlib/Geometry/Euclidean/Sphere/Power.lean
feat(Geometry/Euclidean/Sphere/Power): use side condition `p ∈ line[ℝ, a, b]` (#29344) …
Modified EuclideanGeometry.mul_dist_eq_abs_sub_sq_distView on Github →
2023-05-27 14:09
Mathlib/Geometry/Euclidean/Sphere/Power.lean
feat: port Geometry.Euclidean.Sphere.Power (#4418)
Added EuclideanGeometry.mul_dist_eq_abs_sub_sq_distView on Github →