English
A convenient version of induction on SkewMonoidAlgebra: if a property holds for all single g a and is preserved under addition, then it holds for all elements.
Русский
Удобная версия индукции на SkewMonoidAlgebra: если свойство верно для всех одиночных элементов и сохраняется при суммировании, оно верно и для всех элементов.
LaTeX
$$$$ \\text{Induction'}\\;: \\forall f,\\; p(f) \\text{ under the same hypotheses as above (when } Nonempty G) $$$$
Lean4
/-- Slightly less general but more convenient version of `SkewMonoidAlgebra.induction_on`. -/
@[induction_eliminator]
theorem induction_on' [instNonempty : Nonempty G] {p : SkewMonoidAlgebra k G → Prop} (f : SkewMonoidAlgebra k G)
(single : ∀ g a, p (single g a)) (add : ∀ f g : SkewMonoidAlgebra k G, p f → p g → p (f + g)) : p f :=
induction_on f (by simpa using single (Classical.choice instNonempty) 0) single add
