Commit 2025-12-01 21:12 cfd0058c

feat(Geometry/Euclidean/Circumcenter): circumcenter_ne_point (#32290) Add a lemma that the circumcenter of a simplex (with two or more vertices) does not equal one of its vertices. This uses Simplex ℝ P (n + 1) rather than [NeZero n] because circumradius_pos hasn't yet been converted to the syntactically more general form using NeZero.