English
If you know P(0), P(1), and P(p) for all primes p, and you have a rule that P(a) and P(b) imply P(a·b) for all a,b, then P holds for all natural numbers.
Русский
Если известно P(0), P(1), и P(p) для всех простых p, и есть правило, что P(a) и P(b) ⇒ P(a·b) для любых a,b, тогда P держится для всех 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,\ P(a)\land P(b) \Rightarrow P(ab)) \Rightarrow \forall n:\mathbb{N},\ P(n).$$$
Lean4
/-- Given `P 0`, `P 1`, `P p` for all primes, and a way to extend `P a` and `P b` to
`P (a * b)`, we can define `P` for all natural numbers. -/
@[elab_as_elim]
def recOnMul {motive : ℕ → Sort*} (zero : motive 0) (one : motive 1) (prime : ∀ p, Prime p → motive p)
(mul : ∀ a b, motive a → motive b → motive (a * b)) : ∀ a, motive a :=
recOnPrimeCoprime zero (fun p n hp' => Nat.rec one (fun _ ih => mul _ _ ih (prime p hp')) n)
(fun a b _ _ _ => mul a b)
