Commit 2024-12-01 22:43 8639aea3

View on Github →

feat: Polynomial.map f strictly decreases the degree if f p.leadingCoeff = 0 (#19411) Also make more arguments to degree_map_le implicit. From GrowthInGroups

Estimated changes

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

Modified Mathlib/Algebra/Polynomial/Div.lean

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

modified theorem Polynomial.degree_map_le

added theorem Polynomial.degree_map_lt

modified theorem Polynomial.natDegree_map_le

added theorem Polynomial.natDegree_map_lt'

added theorem Polynomial.natDegree_map_lt

Modified Mathlib/Algebra/Polynomial/Monic.lean

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/Algebra/Polynomial/Splits.lean

Modified Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

Modified Mathlib/RingTheory/EisensteinCriterion.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean

Modified Mathlib/RingTheory/RootsOfUnity/Minpoly.lean