Commit 2023-01-18 17:47 509de852

View on Github →

fix(geometry/euclidean/circumcenter): fix fintype_finite lint error (#18213) Change affine_independent.exists_unique_dist_eq to use finite instead of fintype.

Estimated changes

Modified src/geometry/euclidean/circumcenter.lean

modified theorem affine_independent.exists_unique_dist_eq