English
FreeCommRing α satisfies a structural induction principle: to prove a property for all elements, it suffices to verify it for -1, for generators of the form of b, and that it is preserved under addition and multiplication.
Русский
Свободное кольцо FreeCommRing α удовлетворяет принципу структурной индукции: чтобы доказать свойство для всех элементов, достаточно проверить его на -1, на элементы-генераторы of b, и что свойство сохраняется под сложением и умножением.
LaTeX
$$$ \\text{Let } \\mathcal{M} : \\mathrm{FreeCommRing}(\\alpha) \\to \\mathrm{Prop}. \\quad \\text{If } \\mathcal{M}(-1), \\ \\forall b,\\ \\mathcal{M}(\\mathrm{of}(b)), \\ \\forall x,y,\\ \\mathcal{M}(x) \\land \\mathcal{M}(y) \\Rightarrow \\mathcal{M}(x+y), \\ \\forall x,y,\\ \\mathcal{M}(x) \\land \\mathcal{M}(y) \\Rightarrow \\mathcal{M}(x\\cdot y) \\text{ then } \\forall z,\\ \\mathcal{M}(z). $$$
Lean4
@[elab_as_elim, induction_eliminator]
protected theorem induction_on {motive : FreeCommRing α → Prop} (z : FreeCommRing α) (neg_one : motive (-1))
(of : ∀ b, motive (of b)) (add : ∀ x y, motive x → motive y → motive (x + y))
(mul : ∀ x y, motive x → motive y → motive (x * y)) : motive z :=
have neg : ∀ x, motive x → motive (-x) := fun x ih => neg_one_mul x ▸ mul _ _ neg_one ih
have one : motive 1 := neg_neg (1 : FreeCommRing α) ▸ neg _ neg_one
FreeAbelianGroup.induction_on z (neg_add_cancel (1 : FreeCommRing α) ▸ add _ _ neg_one one)
(fun m => Multiset.induction_on m one fun a _ ih => mul (FreeCommRing.of a) _ (of a) ih) (fun _ ih => neg _ ih) add
