Theorem EuclideanGeometry.Sphere.IsTangentAt.inner_left_eq_zero_of_mem

Modification history

2025-03-31 15:58
Mathlib/Geometry/Euclidean/Sphere/Tangent.lean
feat(Geometry/Euclidean/Sphere/Tangent): tangents to spheres (#22483) …
Added EuclideanGeometry.Sphere.IsTangentAt.inner_left_eq_zero_of_memView on Github →