Commit 2025-11-20 11:57 816f263c

feat(Geometry/Euclidean/Sphere/Tangent): orthRadius-related lemmas (#31731) Add further lemmas about tangency, the common theme of which is that they relate in some way to orthRadius (the full tangent space rather than only a subspace thereof). In particular, give its finrank in a finite-dimensional space and describe tangent spaces that have that finrank, and, not limited to a finite-dimensional space, the two tangent spaces that are parallel to a given orthRadius space.