# Induction principles involving factorizations #

## Definitions #

source
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.

Equations

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

Instances For

source
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.

Equations

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

Instances For

source
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.

Equations

- Nat.recOnPrimeCoprime zero prime_pow coprime a = Nat.recOnPosPrimePosCoprime (fun (p n : ℕ) (h : Nat.Prime p) (x : 0 < n) => prime_pow p n h) zero (prime_pow 2 0 Nat.prime_two) coprime a

Instances For

source
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.

Equations

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

Instances For

source
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
source
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 #

source
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`

source
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`