Commit 2025-11-21 11:20 3b112fd8

refactor(Geometry/Euclidean/Sphere/Tangent): split out orthRadius (#31850) Split the definition and lemmas for orthRadius out of Mathlib.Geometry.Euclidean.Sphere.Tangent into a separate Mathlib.Geometry.Euclidean.Sphere.OrthRadius, in preparation for setting up a further Mathlib.Geometry.Euclidean.Sphere.PolePolar (which will import OrthRadius and be imported by Tangent). There are no changes to definitions, statements or proofs. The doc string for orthRadius (and corresponding description in the module doc string) is updated to reflect that this definition is not just useful at points on the sphere to define tangents but also more generally for defining polars.