Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(geometry/euclidean/basic): `dist_center_eq_dist_center_of_mem_sp…
…here'` (#17390) Add a variant of `dist_center_eq_dist_center_of_mem_sphere`, but with the distances the other way round (analogous to the pair of lemmas `mem_sphere` and `mem_sphere'`).
- Loading branch information