Theorem EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_vsub_mem_and_norm_sq

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) …
Added EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_vsub_mem_and_norm_sqView on Github →