Induction on polynomials #
This file contains lemmas dealing with different flavours of induction on polynomials.
div_X p returns a polynomial
q such that
q * X + C (p.coeff 0) = p.
It can be used in a semiring where the usual division algorithm is not possible
An induction principle for polynomials, valued in Sort* instead of Prop.
- p.rec_on_horner = λ (M0 : M 0) (MC : Π (p : polynomial R) (a : R), p.coeff 0 = 0 → a ≠ 0 → M p → M (p + ⇑polynomial.C a)) (MX : Π (p : polynomial R), p ≠ 0 → M p → M (p * polynomial.X)), dite (p = 0) (λ (hp : p = 0), _.rec_on M0) (λ (hp : ¬p = 0), _.mpr (dite (p.coeff 0 = 0) (λ (hcp0 : p.coeff 0 = 0), _.mpr (_.mpr (_.mpr (MX p.div_X _ (p.div_X.rec_on_horner M0 MC MX))))) (λ (hcp0 : ¬p.coeff 0 = 0), MC ((p.div_X) * polynomial.X) (p.coeff 0) _ hcp0 (dite (p.div_X = 0) (λ (hpX0 : p.div_X = 0), show M ((p.div_X) * polynomial.X), from _.mpr (polynomial.rec_on_horner._main._pack._proof_9.mpr M0)) (λ (hpX0 : ¬p.div_X = 0), MX p.div_X hpX0 (p.div_X.rec_on_horner M0 MC MX))))))
A property holds for all polynomials of positive
degree with coefficients in a semiring
if it holds for
a * X, with
a ∈ R,
p * X, with
p ∈ R[X],
p + a, with
a ∈ R,
p ∈ R[X], with appropriate restrictions on each term.
nat_degree_ne_zero_induction_on for a similar statement involving no explicit multiplication.