Commit 2025-11-17 16:20 dbaa1521

View on Github →

feat(RingTheory): lemmas about scaleRoots (#30984)

Estimated changes

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

added theorem Polynomial.degree_integralNormalization

added theorem Polynomial.integralNormalization_map

added theorem Polynomial.natDegree_integralNormalization

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean

added theorem Polynomial.Factors.scaleRoots

added theorem Polynomial.X_add_C_scaleRoots

added theorem Polynomial.X_sub_C_scaleRoots

added theorem Polynomial.leadingCoeff_scaleRoots

added theorem Polynomial.pow_scaleRoots'

added theorem Polynomial.pow_scaleRoots_of_isReduced

added theorem Polynomial.rootMultiplicity_scaleRoots

added theorem Polynomial.roots_scaleRoots

added theorem Polynomial.scaleRoots_eval_mul