Commit 2023-11-28 11:15 65fce9bb

View on Github →

feat: Add lemmas about Polynomial.scaleRoots. (#8653)

Estimated changes

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

added theorem Polynomial.natDegree_eq_of_natDegree_add_eq_zero

added theorem Polynomial.natDegree_eq_of_natDegree_add_lt_left

added theorem Polynomial.natDegree_eq_of_natDegree_add_lt_right

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean

added theorem Polynomial.add_scaleRoots_of_natDegree_eq

added theorem Polynomial.isCoprime_scaleRoots

added theorem Polynomial.mul_scaleRoots'

added theorem Polynomial.mul_scaleRoots

added theorem Polynomial.mul_scaleRoots_of_noZeroDivisors

added theorem Polynomial.one_scaleRoots

added theorem Polynomial.scaleRoots_C

added theorem Polynomial.scaleRoots_dvd'

added theorem Polynomial.scaleRoots_dvd

added theorem Polynomial.scaleRoots_dvd_iff

added theorem Polynomial.scaleRoots_mul

added theorem Polynomial.scaleRoots_one

added theorem Polynomial.scaleRoots_zero