mathlib
d3e8e0a0 - chore(field_theory/minpoly): Split results from `minpoly.lean` into three files (#18048)

Commit
2 years ago
chore(field_theory/minpoly): Split results from `minpoly.lean` into three files (#18048) In this PR, we split the results contained in `minpoly.lean` into three separate files: `minpoly.basic.lean`, `minpoly.field.lean` and `minpoly.gcd_monoid.lean`. This is helpful for PR #18021.
Author
Parents
Loading