English
In a CancelCommMonoidWithZero α that is a UniqueFactorizationMonoid, there is a principle of induction on primes: if a property holds for 0, for all units, and is preserved under multiplication by a prime factor of a, then it holds for all a.
Русский
В уникальном факторизационном моноиде существует принцип индукции по простым: свойство выполняется для 0, для всех единиц, и сохраняется при умножении на простой делитель; значит, выполняется для всех элементов.
LaTeX
$$$\forall {P:α\to Prop},\ P(0)\to (\forall x\, \mathrm{IsUnit}(x)\to P(x))\to (\forall a\ p:α,\ a \neq 0\land \mathrm{Prime}(p)\to P(a)\to P(p*a))\to P(a).$$$
Lean4
@[elab_as_elim]
theorem induction_on_prime {P : α → Prop} (a : α) (h₁ : P 0) (h₂ : ∀ x : α, IsUnit x → P x)
(h₃ : ∀ a p : α, a ≠ 0 → Prime p → P a → P (p * a)) : P a :=
by
simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime] at h₃
exact WfDvdMonoid.induction_on_irreducible a h₁ h₂ h₃
