Def EuclideanGeometry.Sphere.commonTangents

Modification history

2026-07-24 07:15
Mathlib/Geometry/Euclidean/Sphere/Tangent.lean
chore: add missing `noncomputable` (#41446) …
Deleted EuclideanGeometry.Sphere.commonTangentsView on Github →
2025-03-31 15:58
Mathlib/Geometry/Euclidean/Sphere/Tangent.lean
feat(Geometry/Euclidean/Sphere/Tangent): tangents to spheres (#22483) …
Added EuclideanGeometry.Sphere.commonTangentsView on Github →