Mathlib Changelog
v4
Changelog
About
Github
Theorem
EuclideanGeometry.Sphere.inner_vsub_center_midpoint_vsub
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.inner_vsub_center_midpoint_vsub
View on Github →