Commit 2026-08-20 21:14 64a51849

View on Github →

feat(Algebra/Polynomial): lemmas about polynomial degree (#37956)

Add various small lemmas for computing polynomial degree
Change a hint test to be slightly "harder" since simp gets more powerful

Estimated changes

Modified Mathlib/Algebra/Polynomial/Degree/Defs.lean

modified theorem Polynomial.degree_eq_iff_natDegree_eq

added theorem Polynomial.degree_eq_iff_natDegree_eq_of_neZero

modified theorem Polynomial.degree_eq_iff_natDegree_eq_of_pos

modified theorem Polynomial.natDegree_eq_of_degree_eq_some

Modified Mathlib/Algebra/Polynomial/Degree/Operations.lean

added theorem Polynomial.natDegree_add_one

added theorem Polynomial.natDegree_one_add

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

added theorem Polynomial.natDegree_normalize

Modified Mathlib/Algebra/Polynomial/Monic.lean

added theorem Polynomial.Monic.natDegree_le_of_dvd

Modified MathlibTest/Tactic/Hint/All.lean