Commit 2025-01-03 23:07 166dc0de

View on Github →

feat(Polynomial): (C a * p).degree = p.degree if a * p.leadingCoeff ≠ 0 (#20446) From GrowthInGroups (LeanCamCombi)

Estimated changes

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

added theorem Polynomial.degree_C_mul_of_mul_ne_zero

deleted theorem Polynomial.natDegree_C_mul_eq_of_mul_ne_zero

modified theorem Polynomial.natDegree_C_mul_le

added theorem Polynomial.natDegree_C_mul_of_mul_ne_zero

modified theorem Polynomial.natDegree_mul_C_le

Modified Mathlib/Algebra/Polynomial/Taylor.lean