mathlib

a5abf903 - feat(geometry/euclidean/circumcenter): equal circumspheres among cospherical points (#17572)

feat(geometry/euclidean/circumcenter): equal circumspheres among cospherical points (#17572) We have a series of lemmas that n-simplices among cospherical points in n-space have the same circumcenter and circumradius. Deduce analogous such lemmas that they have the same circumsphere.