circumcenter): fix `fintype_finite` lint error (#18213)

Commit

3 years ago

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

Author

jsm28

Parents

fb319896

mathlib 509de852 - fix(geometry/euclidean/circumcenter): fix `fintype_finite` lint error (#18213)

mathlib
509de852 - fix(geometry/euclidean/circumcenter): fix `fintype_finite` lint error (#18213)