Theorem Polynomial.degree_map_le
Modification history
2024-12-01 22:43
Mathlib/Algebra/Polynomial/Eval/Degree.lean
feat: `Polynomial.map f` strictly decreases the degree if `f p.leadingCoeff = 0` (#19411) …
Modified Polynomial.degree_map_leView on Github →