mathlib3

ae7a88d1 - feat(field_theory/finite/basic): generalize lemma from field to integral domain (#10655)