English
Let P be a predicate on natural numbers. If P(0) and P(p^n) holds for all prime powers p^n, and if P(a) and P(b) imply P(a·b) whenever Coprime(a,b) and a,b > 1, then P(n) holds for every n.
Русский
Пусть P — предикат на ℕ. Если P(0) выполняется и P(p^n) выполняется для всех простых степеней p^n, и если из P(a) и P(b) следует P(ab) для попарно простых a,b > 1, то P(n) выполняется для любого n.
LaTeX
$$$\text{Пусть } P:\mathbb{N}\to\text{Prop}.\ P(0) \\land \forall p,n,\Big(Prime(p) \land 0< n \Rightarrow P(p^n)\Big) \\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
/-- Given `P 0`, `P (p ^ n)` for all prime powers, and a way to extend `P a` and `P b` to
`P (a * b)` when `a, b` are positive coprime, we can define `P` for all natural numbers. -/
@[elab_as_elim]
def recOnPrimeCoprime {motive : ℕ → Sort*} (zero : motive 0) (prime_pow : ∀ p n : ℕ, Prime p → motive (p ^ n))
(coprime : ∀ a b, 1 < a → 1 < b → Coprime a b → motive a → motive b → motive (a * b)) : ∀ a, motive a :=
recOnPosPrimePosCoprime (fun p n h _ => prime_pow p n h) zero (prime_pow 2 0 prime_two) coprime
