English
The free Abelian group on α satisfies a standard induction principle: to prove a property C on all elements, it suffices to prove C(0), C(pure x) for all x, C(-pure x) from C(pure x), and C(x+y) from Cx and Cy.
Русский
Свободная абелева группа на α удовлетворяет стандартному принципу индукции: чтобы доказать свойство C для всех элементов, достаточно доказать C(0), C(pure x) для всех x, из C(pure x) следуют C(-pure x), и из Cx и Cy следует C(x+y).
LaTeX
$$$ \forall {\alpha} {C : FreeAbelianGroup(\alpha) \to \mathrm{Prop}}
( C(0) \to (\forall x, C(\text{pure } x))
\to (\forall x, C(\text{pure } x) \to C(-\text{pure } x))
\to (\forall x y, C x \to C y \to C(x+y))
\to C(z) )$$$
Lean4
@[elab_as_elim]
protected theorem induction_on' {C : FreeAbelianGroup α → Prop} (z : FreeAbelianGroup α) (C0 : C 0)
(C1 : ∀ x, C <| pure x) (Cn : ∀ x, C (pure x) → C (-pure x)) (Cp : ∀ x y, C x → C y → C (x + y)) : C z :=
FreeAbelianGroup.induction_on z C0 C1 Cn Cp
