English
There is an induction principle for FreeAbelianGroup α: to prove a property for all x, it suffices to prove it for zero, generators, and sums and negations.
Русский
Существует принцип индукции по FreeAbelianGroup α: чтобы доказать свойство для любого элемента, достаточно доказать его для нуля, порождающих и сумм/разностей.
LaTeX
$$$\\forall z:\\; FreeAbelianGroup α,\\ C(z)$, где $C$ удовлетворяет условиям на нуле, генераторах и сложении/обратном$$
Lean4
@[elab_as_elim]
protected theorem induction_on {C : FreeAbelianGroup α → Prop} (z : FreeAbelianGroup α) (C0 : C 0) (C1 : ∀ x, C <| of x)
(Cn : ∀ x, C (of x) → C (-of x)) (Cp : ∀ x y, C x → C y → C (x + y)) : C z :=
Quotient.inductionOn' z fun x ↦
Quot.inductionOn x fun L ↦
List.recOn L C0 fun ⟨x, b⟩ _ ih ↦ Bool.recOn b (Cp _ _ (Cn _ (C1 x)) ih) (Cp _ _ (C1 x) ih)
