Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-31 00:27 12a85fac

View on Github →

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).

Estimated changes