Theorems · Definition · number theory

Nat.recOnPosPrimePosCoprime

{motive : ℕ → Sort u_1} →
  ((p n : ℕ) → Nat.Prime p → 0 < n → motive (p ^ n)) →
    motive 0 →
      motive 1 → ((a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)) → (a : ℕ) → motive a

Given P 0, P 1, and P (p ^ n) for positive 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.

Defined in

Mathlib.Data.Nat.Factorization.Induction

Cited by

2 results in Mathlib

Foundations

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