English
A property holds for all polynomials of positive degree with coefficients in a semiring R if it is closed under multiplying by X, adding a nonzero constant, and adding a new polynomial with a shifted constant term, under appropriate degree constraints.
Русский
Свойство выполняется для всех полиномов с положительной степенью над полем R, если оно сохраняется при умножении на X, добавлении ненулевого константного члена и добавлении полинома со сдвинутым константным членом при соответствующих ограничениях по степени.
LaTeX
$$$\\text{degree\\_pos\\_induction\_on}(P, p) := \\text{ (base and inductive steps with } C a \\cdot X, p \\cdot X, p + C a \\text{)}.$$$
Lean4
/-- A property holds for all polynomials of positive `degree` with coefficients in a semiring `R`
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.
See `natDegree_ne_zero_induction_on` for a similar statement involving no explicit multiplication.
-/
@[elab_as_elim]
theorem degree_pos_induction_on {P : R[X] → Prop} (p : R[X]) (h0 : 0 < degree p) (hC : ∀ {a}, a ≠ 0 → P (C a * X))
(hX : ∀ {p}, 0 < degree p → P p → P (p * X)) (hadd : ∀ {p} {a}, 0 < degree p → P p → P (p + C a)) : P p :=
recOnHorner p (fun h => by rw [degree_zero] at h; exact absurd h (by decide))
(fun p a heq0 _ ih h0 =>
(have : 0 < degree p :=
(lt_of_not_ge fun h =>
not_lt_of_ge (degree_C_le (a := a)) <| by rwa [eq_C_of_degree_le_zero h, ← C_add, heq0, zero_add] at h0)
hadd this (ih this)))
(fun p _ ih h0' =>
if h0 : 0 < degree p then hX h0 (ih h0)
else by
rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at h0' ⊢
exact hC fun h : coeff p 0 = 0 => by simp [h] at h0')
h0
