English
Every SkewMonoidAlgebra element satisfies a property provided it is true for 0, closed under single, and closed under addition.
Русский
Каждый элемент SkewMonoidAlgebra удовлетворяет свойству, если оно верно для 0, сохраняется при добавлении единичного элемента и при суммировании.
LaTeX
$$$$ \\bigl( p(0) \\ \\\\land \\\\forall g,a,\; p(SkewMonoidAlgebra.single\; g\; a) \\bigr) \\land \\\\forall f,g,\\; p(f) \\land p(g) \\Rightarrow p(f+g) \\\\Rightarrow \\forall f,\\; p(f) $$$$
Lean4
@[elab_as_elim]
theorem induction_on {p : SkewMonoidAlgebra k G → Prop} (f : SkewMonoidAlgebra k G) (zero : p 0)
(single : ∀ g a, p (single g a)) (add : ∀ f g : SkewMonoidAlgebra k G, p f → p g → p (f + g)) : p f :=
by
rw [← sum_single f, sum_def']
exact Finset.sum_induction _ _ add zero (by simp_all)
