mathlib3

8fd86366 - feat(field_theory/minpoly): add `minpoly.nat_degree_pos` (#6100)

feat(field_theory/minpoly): add `minpoly.nat_degree_pos` (#6100) I needed this lemma and noticed that `minpoly.lean` actually uses this result more than `minpoly.degree_pos` (including in the proof of `degree_pos` itself). So I took the opportunity to golf a couple of proofs.