Commit 2024-06-19 09:36 9b3f65a2

View on Github →

feat(Algebra/Polynomial/RingDivision): Add and simplify some lemmas (#13866) Add natDegree_pos_of_monic_of_ne_one lemma which has a rather simple proof, and deduce the other lemmas from that.

Estimated changes

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

added theorem Polynomial.Monic.natDegree_eq_zero

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

modified theorem Polynomial.Monic.C_dvd_iff_isUnit

added theorem Polynomial.Monic.degree_pos

added theorem Polynomial.Monic.degree_pos_of_not_isUnit

added theorem Polynomial.Monic.natDegree_pos

added theorem Polynomial.Monic.natDegree_pos_of_not_isUnit

deleted theorem Polynomial.degree_pos_of_monic_of_not_isUnit

modified theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic

deleted theorem Polynomial.natDegree_pos_of_monic_of_not_isUnit

modified theorem Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/RingTheory/Polynomial/RationalRoot.lean

added theorem exists_integer_of_is_root_of_monic