Natural number multiplicity

This file contains lemmas about the multiplicity function (the maximum prime power divding a number).

Main results

There are natural number versions of some basic lemmas about multiplicity.

There are also lemmas about the multiplicity of primes in factorials and in binomial coefficients.

theorem nat.multiplicity_eq_card_pow_dvd {m n b : ℕ} (hm1 : m ≠ 1) (hn0 : 0 < n) (hb : n ≤ b) :

multiplicity m n = ↑((finset.filter (λ (i : ℕ), m ^ i ∣ n) (finset.Ico 1 b)).card)

The multiplicity of a divisor m of n, is the cardinality of the set of positive natural numbers i such that p ^ i divides n. The set is expressed by filtering Ico 1 b where b is any bound at least n

source

theorem nat.prime.multiplicity_one {p : ℕ} (hp : nat.prime p) :

multiplicity p 1 = 0

source

theorem nat.prime.multiplicity_mul {p m n : ℕ} (hp : nat.prime p) :

multiplicity p (m * n) = multiplicity p m + multiplicity p n

source

theorem nat.prime.multiplicity_pow {p m n : ℕ} (hp : nat.prime p) :

multiplicity p (m ^ n) = n •ℕ multiplicity p m

source

theorem nat.prime.multiplicity_self {p : ℕ} (hp : nat.prime p) :

multiplicity p p = 1

source

theorem nat.prime.multiplicity_pow_self {p n : ℕ} (hp : nat.prime p) :

multiplicity p (p ^ n) = ↑n

source

theorem nat.prime.multiplicity_fact {p : ℕ} (hp : nat.prime p) {n b : ℕ} (a : n ≤ b) :

multiplicity p n.fact = ↑∑ (i : ℕ) in finset.Ico 1 b, n / p ^ i

The multiplicity of a prime in fact n is the sum of the quotients n / p ^ i. This sum is expressed over the set Ico 1 b where b is any bound at least n

source

theorem nat.prime.pow_dvd_fact_iff {p n r b : ℕ} (hp : nat.prime p) (hbn : n ≤ b) :

p ^ r ∣ n.fact ↔ r ≤ ∑ (i : ℕ) in finset.Ico 1 b, n / p ^ i

A prime power divides fact n iff it is at most the sum of the quotients n / p ^ i. This sum is expressed over the set Ico 1 b where b is any bound at least n

source

theorem nat.prime.multiplicity_choose_aux {p n b k : ℕ} (hp : nat.prime p) (hkn : k ≤ n) :

∑ (i : ℕ) in finset.Ico 1 b, n / p ^ i = ∑ (i : ℕ) in finset.Ico 1 b, k / p ^ i + ∑ (i : ℕ) in finset.Ico 1 b, (n - k) / p ^ i + (finset.filter (λ (i : ℕ), p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (finset.Ico 1 b)).card

source

theorem nat.prime.multiplicity_choose {p n k b : ℕ} (hp : nat.prime p) (hkn : k ≤ n) (hnb : n ≤ b) :

multiplicity p (n.choose k) = ↑((finset.filter (λ (i : ℕ), p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (finset.Ico 1 b)).card)

The multiplity of p in choose n k is the number of carries when k and n - k are added in base p. The set is expressed by filtering Ico 1 b where b is any bound at least n.

source

theorem nat.prime.multiplicity_le_multiplicity_choose_add {p : ℕ} (hp : nat.prime p) (n k : ℕ) :

multiplicity p n ≤ multiplicity p (n.choose k) + multiplicity p k

A lower bound on the multiplicity of p in choose n k.

source

theorem nat.prime.multiplicity_choose_prime_pow {p n k : ℕ} (hp : nat.prime p) (hkn : k ≤ p ^ n) (hk0 : 0 < k) :

multiplicity p ((p ^ n).choose k) + multiplicity p k = ↑n