English
A property M on polynomials holds for every polynomial f with nonzero natDegree provided it holds for basic constructions: adding a constant, adding polynomials, and monomials with nonzero coefficient and nonzero exponent.
Русский
Свойство M на полиномах выполняется для каждого полинома f с ненулевой natDegree, если оно выполняется для базовых конструкций: сложение константы, сложение полиномов и мономы с ненулевым коэффициентом и ненулным степенем.
LaTeX
$$$\\text{natDegree\\_ne\\_zero\\_induction\\_on} : (\\forall f, \\operatorname{natDegree}(f) \\neq 0 \\Rightarrow \\cdots).$$$
Lean4
/-- A property holds for all polynomials of non-zero `natDegree` with coefficients in a
semiring `R` if it holds for
* `p + a`, with `a ∈ R`, `p ∈ R[X]`,
* `p + q`, with `p, q ∈ R[X]`,
* monomials with nonzero coefficient and non-zero exponent,
with appropriate restrictions on each term.
Note that multiplication is "hidden" in the assumption on monomials, so there is no explicit
multiplication in the statement.
See `degree_pos_induction_on` for a similar statement involving more explicit multiplications.
-/
@[elab_as_elim]
theorem natDegree_ne_zero_induction_on {M : R[X] → Prop} {f : R[X]} (f0 : f.natDegree ≠ 0)
(h_C_add : ∀ {a p}, M p → M (C a + p)) (h_add : ∀ {p q}, M p → M q → M (p + q))
(h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (monomial n a)) : M f :=
by
suffices f.natDegree = 0 ∨ M f from Or.recOn this (fun h => (f0 h).elim) id
refine Polynomial.induction_on f ?_ ?_ ?_
· exact fun a => Or.inl (natDegree_C _)
· rintro p q (hp | hp) (hq | hq)
· refine Or.inl ?_
rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
· refine Or.inr ?_
rw [eq_C_of_natDegree_eq_zero hp]
exact h_C_add hq
· refine Or.inr ?_
rw [eq_C_of_natDegree_eq_zero hq, add_comm]
exact h_C_add hp
· exact Or.inr (h_add hp hq)
· intro n a _
by_cases a0 : a = 0
· exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])
· refine Or.inr ?_
rw [C_mul_X_pow_eq_monomial]
exact h_monomial a0 n.succ_ne_zero
