Theorem EuclideanGeometry.Sphere.IsTangentAt.eq_orthRadius_of_finrank_add_one_eq

Modification history

2025-11-20 11:57
Mathlib/Geometry/Euclidean/Sphere/Tangent.lean
feat(Geometry/Euclidean/Sphere/Tangent): `orthRadius`-related lemmas (#31731) …
Added EuclideanGeometry.Sphere.IsTangentAt.eq_orthRadius_of_finrank_add_one_eqView on Github →