Mathlib Changelog
v4
Changelog
About
Github
Theorem
EuclideanGeometry.Sphere.dist_center_midpoint_lt_radius
Modification history
2026-03-10 12:02
Mathlib/Geometry/Euclidean/Sphere/Basic.lean
feat: add dist_center_midpoint_lt_radius for spheres (#35957) …
Added
EuclideanGeometry.Sphere.dist_center_midpoint_lt_radius
View on Github →