English
Let p be a property on MonoidAlgebra R M. If p holds for all basis elements of the form of m, is closed under addition, and is preserved under scalar multiplication by elements of R, then p holds for every element x ∈ MonoidAlgebra R M. This provides an induction principle for MonoidAlgebra.
Русский
Пусть p — свойство для MonoidAlgebra R M. Если p выполняется для всех базисных элементов вида of R M m, свойство сохраняется при сложении и под действием скаляров из R, то p выполняется для любого элемента x ∈ MonoidAlgebra R M. Это индукционный принцип для MonoidAlgebra.
LaTeX
$$$\\forall p : \\mathrm{MonoidAlgebra}(R,M) \\to \\mathrm{Prop},\\ \\forall x \\in \\mathrm{MonoidAlgebra}(R,M),\\ (\\forall m, p(\\mathrm{of}\\, R\\, M\\, m)) \\\\quad\\land\\ (\\forall x,y,\\ p(x) \\to p(y) \\to p(x+y)) \\\\quad\\land\\ (\\forall r: R\\, \\forall x,\\ p(x) \\to p(r \\cdot x)) \\Rightarrow p(x).$$$
Lean4
theorem induction_on {p : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M) (hM : ∀ m, p (of R M 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 1)) (fun x y hf hg => hadd x y hf hg) fun m r ↦ by
simpa using hsmul r (of R M m) (hM m)
