Def EuclideanGeometry.Sphere.tangentSet

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.tangentSet View on Github →