Theorem Polynomial.degree_C_mul_of_mul_ne_zero

Modification history

2025-01-03 23:07

Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

feat(Polynomial): `(C a * p).degree = p.degree` if `a * p.leadingCoeff ≠ 0` (#20446) …

Added Polynomial.degree_C_mul_of_mul_ne_zero View on Github →