Natural number multiplicity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains lemmas about the multiplicity function (the maximum prime power dividing a number) when applied to naturals, in particular calculating it for factorials and binomial coefficients.

Multiplicity calculations #

nat.multiplicity_factorial: Legendre's Theorem. The multiplicity of p in n! is n/p + ... + n/p^b for any b such that n/p^(b + 1) = 0.
nat.multiplicity_factorial_mul: The multiplicity of p in (p * n)! is n more than that of n!.
nat.multiplicity_choose: The multiplicity of p in n.choose k is the number of carries when k andn - k are added in base p.

Other declarations #

nat.multiplicity_eq_card_pow_dvd: The multiplicity of m in n is the number of positive natural numbers i such that m ^ i divides n.
nat.multiplicity_two_factorial_lt: The multiplicity of 2 in n! is strictly less than n.
nat.prime.multiplicity_something: Specialization of multiplicity.something to a prime in the naturals. Avoids having to provide p ≠ 1 and other trivialities, along with translating between prime and nat.prime.

Tags #

Legendre, p-adic

source

theorem nat.multiplicity_eq_card_pow_dvd {m n b : ℕ} (hm : m ≠ 1) (hn : 0 < n) (hb : nat.log m n < b) :

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

The multiplicity of m in n is the number of positive natural numbers i such that m ^ i divides n. This set is expressed by filtering Ico 1 b where b is any bound greater than log m 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_factorial {p : ℕ} (hp : nat.prime p) {n b : ℕ} :

nat.log p n < b → multiplicity p n.factorial = ↑((finset.Ico 1 b).sum (λ (i : ℕ), n / p ^ i))

Legendre's Theorem

The multiplicity of a prime in n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

source

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

multiplicity p (p * (n + 1)).factorial = multiplicity p (p * n).factorial + multiplicity p (n + 1) + 1

The multiplicity of p in (p * (n + 1))! is one more than the sum of the multiplicities of p in (p * n)! and n + 1.

source

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

multiplicity p (p * n).factorial = multiplicity p n.factorial + ↑n

The multiplicity of p in (p * n)! is n more than that of n!.

source

theorem nat.prime.pow_dvd_factorial_iff {p n r b : ℕ} (hp : nat.prime p) (hbn : nat.log p n < b) :

p ^ r ∣ n.factorial ↔ r ≤ (finset.Ico 1 b).sum (λ (i : ℕ), n / p ^ i)

A prime power divides 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 greater than log p n

source

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

multiplicity p n.factorial ≤ ↑(n / (p - 1))

source

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

(finset.Ico 1 b).sum (λ (i : ℕ), n / p ^ i) = (finset.Ico 1 b).sum (λ (i : ℕ), k / p ^ i) + (finset.Ico 1 b).sum (λ (i : ℕ), (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 : nat.log p 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 multiplicity 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 greater than log p 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_add_multiplicity {p n k : ℕ} (hp : nat.prime p) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) :

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

source

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

multiplicity p ((p ^ n).choose k) = ↑(n - (multiplicity p k).get _)

source

theorem nat.prime.dvd_choose_pow {p n k : ℕ} (hp : nat.prime p) (hk : k ≠ 0) (hkp : k ≠ p ^ n) :

p ∣ (p ^ n).choose k

source

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

p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n

source

theorem nat.multiplicity_two_factorial_lt {n : ℕ} (h : n ≠ 0) :

multiplicity 2 n.factorial < ↑n