Theorems · Theorem · number theory

Nat.prime_composite_induction

∀ {motive : ℕ → Prop},
  motive 0 →
    motive 1 →
      (∀ (p : ℕ), Nat.Prime p → motive p) →
        (∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)) → ∀ (n : ℕ), motive n

Defined in

Mathlib.Data.Nat.Factorization.Induction

Cited by

1 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound