Induction principles involving factorizations

Definitions

def Nat.recOnPrimePow {P : ℕ → Sort u_1} (h0 : P 0) (h1 : P 1) (h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)) (a : ℕ) : P a

Given P 0, P 1 and a way to extend P a to P (p ^ n * a) for prime p not dividing a, we can define P for all natural numbers.

def Nat.recOnPosPrimePosCoprime {P : ℕ → Sort u_1} (hp : (p n : ℕ) → Prime p → 0 < n → P (p ^ n)) (h0 : P 0) (h1 : P 1) (h : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → P a → P b → P (a * b)) (a : ℕ) : P 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.

def Nat.recOnPrimeCoprime {P : ℕ → Sort u_1} (h0 : P 0) (hp : (p n : ℕ) → Prime p → P (p ^ n)) (h : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → P a → P b → P (a * b)) (a : ℕ) : P a

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.

def Nat.recOnMul {P : ℕ → Sort u_1} (h0 : P 0) (h1 : P 1) (hp : (p : ℕ) → Prime p → P p) (h : (a b : ℕ) → P a → P b → P (a * b)) (a : ℕ) : P a

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.

def Nat.recOnMul.hp'' {P : ℕ → Sort u_1} (h1 : P 1) (hp : (p : ℕ) → Prime p → P p) (h : (a b : ℕ) → P a → P b → P (a * b)) (p n : ℕ) (hp' : Prime p) : P (p ^ n)

The predicate holds on prime powers

theorem induction_on_primes {P : ℕ → Prop} (h₀ : P 0) (h₁ : P 1) (h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)) (n : ℕ) : P n

theorem Nat.prime_composite_induction {P : ℕ → Prop} (zero : P 0) (one : P 1) (prime : ∀ (p : ℕ), Prime p → P p) (composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)) (n : ℕ) : P n

Lemmas on multiplicative functions

theorem Nat.multiplicative_factorization {β : Type u_1} [CommMonoid β] (f : ℕ → β) (h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) (hf : f 1 = 1) {n : ℕ} : n ≠ 0 → f n = n.factorization.prod fun (p k : ℕ) => f (p ^ k)

For any multiplicative function f with f 1 = 1 and any n ≠ 0, we can evaluate f n by evaluating f at p ^ k over the factorization of n

theorem Nat.multiplicative_factorization' {n : ℕ} {β : Type u_1} [CommMonoid β] (f : ℕ → β) (h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) : f n = n.factorization.prod fun (p k : ℕ) => f (p ^ k)

For any multiplicative function f with f 1 = 1 and f 0 = 1, we can evaluate f n by evaluating f at p ^ k over the factorization of n