mathlib3

640ba6c8 - feat(geometry/euclidean): cospherical points (#4178)

feat(geometry/euclidean): cospherical points (#4178) Define cospherical points in a Euclidean space (the general-dimension version of the two-dimensional concept of a set of points being concyclic) and prove some very basic lemmas about them.