Theorem EuclideanGeometry.Sphere.self_mem_orthRadius

Modification history

2026-03-27 17:02
Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean
feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars (#31891) …
Modified EuclideanGeometry.Sphere.self_mem_orthRadiusView on Github →
2025-11-21 11:20
Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean
refactor(Geometry/Euclidean/Sphere/Tangent): split out `orthRadius` (#31850) …
Modified EuclideanGeometry.Sphere.self_mem_orthRadiusView 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.self_mem_orthRadiusView on Github →