Mathlib Changelog
v4
Changelog
About
Github
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