Commit 2024-12-02 07:36 675c28ea

View on Github →

feat(Polynomial): new lemmas and noncommutative generalizations (#19665) In Algebra/Polynomial/Eval/Degree.lean: two new lemmas about the coefficients and zero-ness of the composition of a polynomial with C r * X. Noncommutative generalizations: Algebra/Polynomial/Degree/Lemmas.lean: two lemmas RingTheory/Polynomial/Tower.lean: one lemma RingTheory/Polynomial/IntegralNormalization.lean: add of_commute versions of two lemmas similar to Polynomial.scaleRoots_eval₂_mul_of_commute and generalize one lemma.

Estimated changes

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

modified theorem Polynomial.comp_eq_zero_iff

modified theorem Polynomial.comp_neg_X_leadingCoeff_eq

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

added theorem Polynomial.comp_C_mul_X_coeff

added theorem Polynomial.comp_C_mul_X_eq_zero_iff

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

modified theorem Polynomial.integralNormalization_aeval_eq_zero

added theorem Polynomial.integralNormalization_eval₂_eq_zero_of_commute

added theorem Polynomial.integralNormalization_eval₂_leadingCoeff_mul_of_commute

Modified Mathlib/RingTheory/Polynomial/Tower.lean

modified theorem Polynomial.eval_map_algebraMap