Partial degrees of the image of a polynomial under a coefficient map #
A ring homomorphism f : R →+* S applied to the coefficients of a multivariate polynomial P
can only remove monomials, so it does not raise any partial degree. This is the partial-degree
form of Mathlib's MvPolynomial.degrees_map_le.
Main results #
MvPolynomial.degreeOf_map_le:degreeOf i (P.map f) ≤ degreeOf i P.
theorem
MvPolynomial.degreeOf_map_le
{σ : Type u_1}
{R : Type u_2}
{S : Type u_3}
[CommSemiring R]
[CommSemiring S]
(f : R →+* S)
(P : MvPolynomial σ R)
(i : σ)
:
Mapping the coefficients of P does not raise its degree in Xᵢ.