Erase the leading term of a univariate polynomial #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
erase_lead serves as reduction step in an induction, shaving off one monomial from a polynomial.
The definition is set up so that it does not mention subtraction in the definition,
and thus works for polynomials over semirings as well as rings.
erase_lead f for a polynomial
f is the polynomial obtained by
f the leading term of
An induction lemma for polynomials. It takes a natural number
N as a parameter, that is
required to be at least as big as the
nat_degree of the polynomial. This is useful to prove
results where you want to change each term in a polynomial to something else depending on the
nat_degree of the polynomial itself and not on the specific
nat_degree of each term.
φ : R[x] → S[x] be an additive map,
k : ℕ a bound, and
fu : ℕ → ℕ a
"sufficiently monotone" map. Assume also that
0all monomials of degree less than
φmaps each monomial
R[x]to a polynomial
φ mof degree
fu (deg m). Then,
φmaps each polynomial
R[x]to a polynomial of degree
fu (deg p).