mathlib documentation

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 #

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 : ), nat.prime p¬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
  • nat.rec_on_prime_pow h0 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 : := padic_val_nat p (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 : ), nat.prime p0 < 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
def nat.rec_on_prime_coprime {P : Sort u_1} (h0 : P 0) (hp : Π (p n : ), nat.prime pP (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 : ), nat.prime pP 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