Commit 2023-03-13 12:12 54ea1b19

View on Github →

feat: Port RingTheory.Polynomial.ScaleRoots (#2841)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/ScaleRoots.lean

added theorem Polynomial.coeff_scaleRoots

added theorem Polynomial.coeff_scaleRoots_natDegree

added theorem Polynomial.degree_scaleRoots

added theorem Polynomial.map_scaleRoots

added theorem Polynomial.monic_scaleRoots_iff

added theorem Polynomial.natDegree_scaleRoots

added theorem Polynomial.scaleRoots_aeval_eq_zero

added theorem Polynomial.scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero

added theorem Polynomial.scaleRoots_eval₂_eq_zero

added theorem Polynomial.scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero

added theorem Polynomial.scaleRoots_eval₂_mul

added theorem Polynomial.scaleRoots_ne_zero

added theorem Polynomial.support_scaleRoots_eq

added theorem Polynomial.support_scaleRoots_le

added theorem Polynomial.zero_scaleRoots