Commit 2025-09-21 21:23 61d33a46

feat(Geometry/Euclidean/Sphere/Power): use side condition p ∈ line[ℝ, a, b] (#29344) This PR changes the side condition used in theorems about Sphere.power to be p ∈ line[ℝ, a, b]. This is symmetric in a and b, and more general than the current condition. TODO (in this PR?): add some basic lemmas about p ∈ line[ℝ, a, b]. TODO (in another PR): prove the power theorems about Sphere.secondInter, which is more general in the sense that it also includes the case where a and b coincide, and then p is on the tangent line.