# Commit 2020-08-15 22:09 8f75f963

View on Github →feat(geometry/euclidean): circumcenter and circumradius (#3693)
Show that every simplex in a Euclidean affine space has a unique
circumcenter (in the affine subspace spanned by that simplex) and
circumradius. There are four main pieces, which all seem closely
enough related to put them all together in the same PR. Both (b) and
(c) have quite long proofs, but I don't see obvious pieces to extract
from them.
(a) Various lemmas about `orthogonal_projection`

in relation to points
equidistant from families of points.
(b) The induction step for the existence and uniqueness of the
(circumcenter, circumradius) pair, `exists_unique_dist_eq_of_insert`

(this is actually slightly more general than is needed for the
induction; it includes going from a set of points that has a unique
circumcenter and circumradius despite being infinite or not affine
independent, to such a unique circumcenter and circumradius when
another point is added outside their affine subspace). This is
essentially just a calculation using an explicit expression for the
distance of the circumcenter of the new set of points from its
orthogonal projection, but still involves quite a lot of manipulation
to get things down to a form `field_simp, ring`

can handle.
(c) The actual induction
`exists_unique_dist_eq_of_affine_independent`

, giving a unique
(circumcenter, circumradius) pair for for any affine independent
family indexed by a `fintype`

, by induction on the cardinality of that
`fintype`

and using the result from (b). Given (b), this is
essentially a lot of manipulation of trivialities.
(d) Extracting definitions and basic properties of `circumcenter`

and
`circumradius`

from the previous result.