Erase the leading term of a univariate polynomial #
eraseLead f: the polynomial
f - leading term of f
eraseLead 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.
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).