Commit 2021-02-09 05:58 8fd86366
View on Github →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.