Commit 2022-10-05 09:32 a4d24238

feat(geometry/euclidean/basic): bundled spheres (#16184) Define a bundled sphere structure, for various uses in Euclidean geometry where it's convenient to pass around center and radius together. Some basic API is set up for this structure, including sphere versions of a few existing lemmas that could naturally be expressed in that way. The construction of circumcenter and circumradius is also changed to pass around a sphere instead of using P × ℝ. It is likely that other existing lemmas can usefully have bundled sphere versions added in followups. Certainly there are plenty of other definitions and results about spheres that can usefully be built up on top of this basic API. Notes:

• As with cospherical, the definition and some of the most basic lemmas don't actually need anything more than the metric space structure. sphere is defined alongside cospherical, but it would also be reasonable to define both in some metric space file. In that case, the name of sphere would need to change to avoid conflicts with the existing metric.sphere (which is part of a family of unbundled definitions with metric.ball and metric.closed_ball, so should probably remain as-is).
• The definition doesn't include any non-degeneracy conditions, so avoiding the need for users to prove such conditions when constructing a sphere for a lemma that doesn't need them. Note that the base case for the induction constructing the circumsphere uses a radius of zero.
• I haven't forgotten the discussion in #4088 of simplifying the proof of eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two using bundled spheres, a definition of the radical subspace and a proof that a one-dimensional sphere has at most two points (so ending up proving the unbundled lemma using the bundled one rather than vice versa), but I think quite a lot more API about power of a point and radical subspaces would still need adding before that could be done.