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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Nat.recOnPrimeCoprime h0 hp h a = Nat.recOnPosPrimePosCoprime (fun (p n : ℕ) (h : Nat.Prime p) (x : 0 < n) => hp p n h) h0 (hp 2 0 Nat.prime_two) h a

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.

Equations

• Nat.recOnMul h0 h1 hp h a = Nat.recOnPrimeCoprime h0 (Nat.recOnMul.hp'' h1 hp h) (fun (a b : ℕ) (x : 1 < a) (x : 1 < b) (x : a.Coprime b) => h a b) a

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

Equations

• Nat.recOnMul.hp'' h1 hp h p 0 hp' = h1
• Nat.recOnMul.hp'' h1 hp h p n_2.succ hp' = h (p.pow n_2) p (Nat.recOnMul.hp'' h1 hp h p n_2 hp') (hp p hp')

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