English
There is a linear-induction principle for MonoidAlgebra: to prove a property p for all x, it suffices to prove it for 0, show it is preserved under addition, and prove it for all single m r.
Русский
Существует линейная индукция для MonoidAlgebra: чтобы доказать свойство p для всех x, достаточно доказать его для 0, показать сохранение под сложением и доказать для каждого single m r.
LaTeX
$$$\\text{induction\_linear} : \\forall p: MonoidAlgebra(R,M)\\to \\mathrm{Prop},\\ p(0)\\to (\\forall x,y, p(x)\\to p(y)\\to p(x+y))\\to (\\forall m r, p(\\mathrm{single}(m,r)))\\to p(x)$$$
Lean4
@[to_additive (attr := elab_as_elim)]
theorem induction_linear {p : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M) (zero : p 0)
(add : ∀ x y : MonoidAlgebra R M, p x → p y → p (x + y)) (single : ∀ m r, p (single m r)) : p x :=
Finsupp.induction_linear x zero (fun _ _ ↦ add _ _) (fun _ _ ↦ single _ _)
