mathlib3

12a85fac - chore(field_theory/finite/basic): move a lemma (#19130)

chore(field_theory/finite/basic): move a lemma (#19130) Moving one instance we can erase `field_theory.splitting_field` from the imports of `field_theory.finite.basic)`.