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.
