English
Let P be a property of PolynomialModule R M. If P holds for 0, is preserved under addition, and holds for all singleton polynomials, then P holds for every element of PolynomialModule R M.
Русский
Пусть P — свойство PolynomialModule R M. Если P верно для 0, сохраняется при сложении и верно для всех одиноких полиномов, то P верно для любого элемента PolynomialModule R M.
LaTeX
$$\forall {P : PolynomialModule R M → Prop}, P(0) ∧ (\forall f g, P(f) → P(g) → P(f+g)) ∧ (\forall a b, P(single R a b)) → (\forall f, P(f))$$
Lean4
@[elab_as_elim]
theorem induction_linear {motive : PolynomialModule R M → Prop} (f : PolynomialModule R M) (zero : motive 0)
(add : ∀ f g, motive f → motive g → motive (f + g)) (single : ∀ a b, motive (single R a b)) : motive f :=
Finsupp.induction_linear f zero add single
