Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 20:53 a5abf903

View on Github →

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.

Estimated changes