English
Let C be a property of elements of FreeRing α. If C holds for -1, holds for all of b (b ∈ α), and is closed under addition and multiplication, then C holds for every z ∈ FreeRing α.
Русский
Пусть C — свойство элементов FreeRing α. Если C верно для -1, C верно для каждого of b (для всех b ∈ α), и C замкнуто относительно сложения и умножения, то C верно для любого z ∈ FreeRing α.
LaTeX
$$$$\forall C:\\mathrm{FreeRing}(\alpha) \to \mathrm{Prop},\; C(-1) \to (\forall b, C(\\mathrm{of}(b))) \\to (\\forall x y, C(x) \to C(y) \to C(x+y)) \\to (\\forall x y, C(x) \to C(y) \to C(x * y)) \\to C(z).$$$$
Lean4
@[elab_as_elim, induction_eliminator]
protected theorem induction_on {C : FreeRing α → Prop} (z : FreeRing α) (hn1 : C (-1)) (hb : ∀ b, C (of b))
(ha : ∀ x y, C x → C y → C (x + y)) (hm : ∀ x y, C x → C y → C (x * y)) : C z :=
have hn : ∀ x, C x → C (-x) := fun x ih => neg_one_mul x ▸ hm _ _ hn1 ih
have h1 : C 1 := neg_neg (1 : FreeRing α) ▸ hn _ hn1
FreeAbelianGroup.induction_on z (neg_add_cancel (1 : FreeRing α) ▸ ha _ _ hn1 h1)
(fun m => List.recOn m h1 fun a _ ih => hm _ _ (hb a) ih) (fun _ ih => hn _ ih) ha
