English
Let α be a commutative monoid with zero that is a WfDvdMonoid. For any property P on α, if P(0) holds, P(u) holds for every unit u, and whenever a ≠ 0 and i is irreducible and P(a) holds, then P(i a) also holds, then P(a) holds for every a ∈ α.
Русский
Пусть α — коммутативный моноид с нулём, удовлетворяющий условию хорошо основанной делимости. Для любого свойства P на α, если P(0) истинно, и для каждого единичного элемента u верно P(u), и если при a ≠ 0 и ирредуцируемом i имеем P(a) ⇒ P(i a), то P(a) истинно для всех a.
LaTeX
$$@[elab_as_elim]\ntheorem induction_on_irreducible {motive : α → Prop} (a : α) (zero : motive 0) (unit : ∀ u : α, IsUnit u → motive u)\n (mul : ∀ a i : α, a ≠ 0 → Irreducible i → motive a → motive (i * a)) : motive a$$
Lean4
@[elab_as_elim]
theorem induction_on_irreducible {motive : α → Prop} (a : α) (zero : motive 0) (unit : ∀ u : α, IsUnit u → motive u)
(mul : ∀ a i : α, a ≠ 0 → Irreducible i → motive a → motive (i * a)) : motive a :=
haveI := Classical.dec
wellFounded_dvdNotUnit.fix
(fun a ih =>
if ha0 : a = 0 then ha0.substr zero
else
if hau : IsUnit a then unit a hau
else
let ⟨i, i_irred, b, hb⟩ := exists_irreducible_factor hau ha0
let hb0 : b ≠ 0 := ne_zero_of_dvd_ne_zero ha0 ⟨i, mul_comm i b ▸ hb⟩
hb.symm ▸ mul b i hb0 i_irred <| ih b ⟨hb0, i, i_irred.1, mul_comm i b ▸ hb⟩)
a
