induction_on — Mathlib

English

Let R be a semiring and let P be a property of polynomials, P: R[X] → Prop. If P holds for all constant polynomials of the form C a, P is closed under addition, and P is closed under the standard monomial-growth step P(C a X^n) → P(C a X^{n+1}) for every n and a, then P holds for every polynomial p ∈ R[X]. In other words, any property that is preserved under addition and can be verified on monomials is automatically true for all polynomials.

Русский

Пусть R — полугруппа с умножением, а P — свойство многочленов: P: R[X] → Prop. Если P выполняется для всех константных многочленов C a, свойство P сохраняется при сложении (p + q) и выполняется переход P(C a X^n) → P(C a X^{n+1}) для любых n и a, тогда P(p) выполняется для любого p ∈ R[X]. Другими словами, свойство, сохраняющееся при суммировании и позвонку на мономах, автоматически верно для всех многочленов.

LaTeX

$$$\\forall R [Semiring\ \,R],\\forall (motive: R[X] \\to Prop),\\Big( (\\forall a, motive(C\\ a)) \\land (\\forall p\\ q, motive(p) \\to motive(q) \\to motive(p+q)) \\land (\\forall n\\ (a:\\,R), motive(Polynomial.C\\ a * X^n) \\to motive(Polynomial.C\\ a * X^{n+1}) ) \\Big) \\to \\forall p:\\,R[X],\\ motive(p).$$

Lean4

@[elab_as_elim]
protected theorem induction_on {motive : R[X] → Prop} (p : R[X]) (C : ∀ a, motive (C a))
    (add : ∀ p q, motive p → motive q → motive (p + q))
    (monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))) :
    motive p :=
  by
  have A : ∀ {n : ℕ} {a}, motive (Polynomial.C a * X ^ n) :=
    by
    intro n a
    induction n with
    | zero => rw [pow_zero, mul_one]; exact C a
    | succ n ih => exact monomial _ _ ih
  have B : ∀ s : Finset ℕ, motive (s.sum fun n : ℕ => Polynomial.C (p.coeff n) * X ^ n) :=
    by
    apply Finset.induction
    · convert C 0
      exact C_0.symm
    · intro n s ns ih
      rw [sum_insert ns]
      exact add _ _ A ih
  rw [← sum_C_mul_X_pow_eq p, Polynomial.sum]
  exact B (support p)

Похожие утверждения