English
Let P be a predicate on natural numbers. If P(0), P(1) hold, and for every prime p we have P(p) and for all a,b with Coprime(a,b), P(a) and P(b) imply P(a·b), then P(n) holds for every n.
Русский
Пусть P — предикат на ℕ. Если P(0), P(1) истинны, и для каждого простого p верно P(p), а также для попарно простых a,b верно P(a) и P(b) ⇒ P(ab), тогда P(n) для всех n.
LaTeX
$$$\forall P:\mathbb{N}\to\text{Prop},\ P(0)\land P(1)\land (\forall p\ prime(p) \Rightarrow P(p))\land (\forall a,b>1,\ Coprime(a,b) \Rightarrow P(a)\land P(b) \Rightarrow P(ab)) \Rightarrow \forall n:\mathbb{N},\ P(n).$$$
Lean4
theorem _root_.induction_on_primes {motive : ℕ → Prop} (zero : motive 0) (one : motive 1)
(prime_mul : ∀ p a : ℕ, p.Prime → motive a → motive (p * a)) : ∀ n, motive n :=
by
refine recOnPrimePow zero one ?_
rintro a p n hp - - ha
induction n with
| zero => simpa using ha
| succ n ih =>
rw [pow_succ', mul_assoc]
exact prime_mul _ _ hp ih
