English
Let motive be a property assigned to multivariate polynomials. If the property holds for all constant polynomials and is preserved under addition and under multiplication by a variable X_n, then the property holds for every multivariate polynomial.
Русский
Пусть для множества переменных σ и кольца R задано свойство motive на многочленах MvPolynomial(σ, R). Если оно выполняется для всех константных полиномов и сохраняется при сложении и умножении на переменную X_n, то выполняется для любого многочлена MvPolynomial.
LaTeX
$$$\\\\forall p: MvPolynomial\\\\,\\\\sigma\\\\,R\\\\, \\\\Big( \\\\big( \\\\forall a, motive(C a) \\\\big) \\\\land \\\\big( \\\\forall p\\\\, q, motive(p) \\\\land motive(q) \\\\Rightarrow motive(p + q) \\\\big) \\\\land \\\\big( \\\\forall p\\\\, n, motive(p) \\\\Rightarrow motive(p * X n) \\\\big) \\\\Big) \\\\Rightarrow motive(p) $$$
Lean4
/-- Analog of `Polynomial.induction_on`.
If a property holds for any constant polynomial
and is preserved under addition and multiplication by variables
then it holds for all multivariate polynomials.
-/
@[recursor 5]
theorem induction_on {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ a, motive (C a))
(add : ∀ p q, motive p → motive q → motive (p + q)) (mul_X : ∀ p n, motive p → motive (p * X n)) : motive p :=
induction_on'' p C (fun a b f _ha _hb hf hm => add (monomial a b) f hm hf) mul_X
