Theorem EuclideanGeometry.inner_vsub_center_vsub_pos

Modification history

2026-03-11 03:16
Mathlib/Geometry/Euclidean/Sphere/Basic.lean
feat(Geometry.Euclidean.Sphere): inner product of chord with radius vector is negative (#36241) …
Added EuclideanGeometry.inner_vsub_center_vsub_posView on Github →