Induction principles involving factorizations

Definitions

def Nat.recOnPrimePow {motive : ℕ → Sort u_1} (zero : motive 0) (one : motive 1) (prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)) (a : ℕ) : motive 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 {motive : ℕ → Sort u_1} (prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)) (zero : motive 0) (one : motive 1) (coprime : (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.

def Nat.recOnPrimeCoprime {motive : ℕ → Sort u_1} (zero : motive 0) (prime_pow : (p n : ℕ) → Prime p → motive (p ^ n)) (coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)) (a : ℕ) : motive 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 {motive : ℕ → Sort u_1} (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

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.

theorem induction_on_primes {motive : ℕ → Prop} (zero : motive 0) (one : motive 1) (prime_mul : ∀ (p a : ℕ), Nat.Prime p → motive a → motive (p * a)) (n : ℕ) : motive n

theorem Nat.prime_composite_induction {motive : ℕ → Prop} (zero : motive 0) (one : motive 1) (prime : ∀ (p : ℕ), Prime p → motive p) (composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)) (n : ℕ) : motive 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