data.nat.mul_ind

# Multiplicative induction principles for ℕ #

This file provides three (closely linked) induction principles for ℕ, commonly used for proofs about multiplicative functions, such as the totient function and the Möbius function.

## Main definitions #

• nat.rec_on_prime_pow: Given P 0, P 1 and a way to extend P a to P (p ^ k * a), you can define P for all natural numbers.
• nat.rec_on_prime_coprime: Given P 0, P (p ^ k) for all p prime, and a way to extend P a and P b to P (a * b) when a, b are coprime, you can define P for all natural numbers.
• nat.rec_on_pos_prime_coprime: Given P 0, P 1, and P (p ^ k) for positive prime powers, and a way to extend P a and P b to P (a * b) when a, b are coprime, you can define P for all natural numbers.
• nat.rec_on_mul: Given P 0, P 1, P p for all primes, and a proof that you can extend P a and P b to P (a * b), you can define P for all natural numbers.

## Implementation notes #

The proofs use padic_val_nat; however, we have padic_val_nat p = nat.log p \$ nat.gcd k (p ^ k) for any p ∣ k, which requires far less imports - the API isn't there though; however, this is why it's in data even though we import number_theory; it's not a particularly deep theorem.

## TODO: #

Extend these results to any normalization_monoid with unique factorization.

def nat.rec_on_prime_pow {P : Sort u_1} (h0 : P 0) (h1 : P 1) (h : Π (a p n : ), ¬p aP aP ((p ^ n) * a)) (a : ) :
P a

Given P 0, P 1 and a way to extend P a to P (p ^ k * a), you can define P for all natural numbers.

Equations
• h1 h = λ (a : ), a.strong_rec_on (λ (n : ), nat.rec_on_prime_pow._match_1 h0 h1 h n)
• nat.rec_on_prime_pow._match_1 h0 h1 h (k + 2) = λ (hk : Π (m : ), m < k + 2P m), let p : := (k + 2).min_fac, t : := (k + 2) in _.mpr (h ((k + 2) / p ^ t) p t _ _ (hk ((k + 2) / p ^ t) _))
• nat.rec_on_prime_pow._match_1 h0 h1 h 1 = λ (_x : Π (m : ), m < 1P m), h1
• nat.rec_on_prime_pow._match_1 h0 h1 h 0 = λ (_x : Π (m : ), m < 0P m), h0
def nat.rec_on_pos_prime_coprime {P : Sort u_1} (hp : Π (p n : ), 0 < nP (p ^ n)) (h0 : P 0) (h1 : P 1) (h : Π (a b : ), a.coprime bP aP bP (a * b)) (a : ) :
P a

Given P 0, P 1, and P (p ^ k) for positive prime powers, and a way to extend P a and P b to P (a * b) when a, b are coprime, you can define P for all natural numbers.

Equations
• h1 h = h1 (λ (a p n : ) (hp' : (hpa : ¬p a) (ha : P a), h (p ^ n) a _ (dite (n = 0) (λ (h : n = 0), eq.rec h1 _) (λ (h : ¬n = 0), hp p n hp' _)) ha)
def nat.rec_on_prime_coprime {P : Sort u_1} (h0 : P 0) (hp : Π (p n : ), P (p ^ n)) (h : Π (a b : ), a.coprime bP aP bP (a * b)) (a : ) :
P a

Given P 0, P (p ^ k) for all prime powers, and a way to extend P a and P b to P (a * b) when a, b are coprime, you can define P for all natural numbers.

Equations
def nat.rec_on_mul {P : Sort u_1} (h0 : P 0) (h1 : P 1) (hp : Π (p : ), P p) (h : Π (a b : ), P aP bP (a * b)) (a : ) :
P a

Given P 0, P 1, P p for all primes, and a proof that you can extend P a and P b to P (a * b), you can define P for all natural numbers.

Equations
• h1 hp h = let hp : Π (p n : ), P (p ^ n) := λ (p n : ) (hp' : , nat.rec_on_mul._match_1 h1 hp h p hp' n in (λ (a b : ) (_x : a.coprime b), h a b)
• nat.rec_on_mul._match_1 h1 hp h p hp' (n + 1) = h p (p ^ n.add 0) (hp p hp') (nat.rec_on_mul._match_1 h1 hp h p hp' n)
• nat.rec_on_mul._match_1 h1 hp h p hp' 0 = h1