English
Let M be an additive monoid and R a semiring. For a predicate P on the monoid algebra R[M], if P holds on all basis elements corresponding to each m ∈ M, if P is closed under addition, and closed under scalar multiplication by R, then P holds for every element of R[M].
Русский
Пусть M — аддитивный моноид, R — полугруппа. Пусть P — свойство над элементами алгебры R[M]. Если P выполняется для всех базисных элементов, соответствующих m ∈ M, если P сохраняется при сложении и при умножении на скаляры из R, то P выполняется для любого элемента R[M].
LaTeX
$$$\\forall P: R[M] \\to \\mathrm{Prop},\\ (\\forall m\\in M,\; P(\\operatorname{of}R M \\; (.\\operatorname{ofAdd} m))) \\land\\ (\\forall x,y\\; P(x) \\to P(y) \\to P(x+y)) \\land\\ (\\forall r\\in R, x\\; P(x) \\to P(r\\cdot x)) \\Rightarrow P(x)$ for any $x\\in R[M]$.$$
Lean4
theorem induction_on [AddMonoid M] {p : R[M] → Prop} (x : R[M]) (hM : ∀ m, p (of R M <| .ofAdd m))
(hadd : ∀ x y : MonoidAlgebra R M, p x → p y → p (x + y)) (hsmul : ∀ (r : R) (x), p x → p (r • x)) : p x :=
Finsupp.induction_linear x (by simpa using hsmul 0 (of R M 1) (hM 0)) (fun x y hf hg ↦ hadd x y hf hg) fun m r ↦ by
simpa using hsmul r (of R M m) (hM m)
