Commit 2022-10-13 06:01 8f82d25e

feat(geometry/euclidean/basic): concyclic (#16927) Define a set of points to be concyclic if it is cospherical and coplanar. I don't expect that much use of this definition, as opposed to the separate cospherical and coplanar pieces, in mathlib, but it's intended to allow formal statements of results involving concyclic points that correspond more closely to the informal statements.