Theorem EuclideanGeometry.Sphere.orthRadius_map

Modification history

2025-11-21 11:20
Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean
refactor(Geometry/Euclidean/Sphere/Tangent): split out `orthRadius` (#31850) …
Modified EuclideanGeometry.Sphere.orthRadius_mapView on Github →
2025-11-20 11:57
Mathlib/Geometry/Euclidean/Sphere/Tangent.lean
feat(Geometry/Euclidean/Sphere/Tangent): `orthRadius`-related lemmas (#31731) …
Added EuclideanGeometry.Sphere.orthRadius_mapView on Github →