Documentation

Mathlib.Data.Nat.Multiplicity

Natural number multiplicity #

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 #

Other declarations #

Tags #

Legendre, p-adic

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.card (Finset.filter (fun i => m ^ i n) (Finset.Ico 1 b)))

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.

theorem Nat.Prime.multiplicity_mul {p : } {m : } {n : } (hp : Nat.Prime p) :
theorem Nat.Prime.multiplicity_pow {p : } {m : } {n : } (hp : Nat.Prime p) :
theorem Nat.Prime.multiplicity_pow_self {p : } {n : } (hp : Nat.Prime p) :
multiplicity p (p ^ n) = n
theorem Nat.Prime.multiplicity_factorial {p : } (hp : Nat.Prime p) {n : } {b : } :
Nat.log p n < bmultiplicity p (Nat.factorial n) = ↑(Finset.sum (Finset.Ico 1 b) fun 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.

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.

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

theorem Nat.Prime.pow_dvd_factorial_iff {p : } {n : } {r : } {b : } (hp : Nat.Prime p) (hbn : Nat.log p n < b) :
p ^ r Nat.factorial n r Finset.sum (Finset.Ico 1 b) fun 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

theorem Nat.Prime.multiplicity_choose_aux {p : } {n : } {b : } {k : } (hp : Nat.Prime p) (hkn : k n) :
(Finset.sum (Finset.Ico 1 b) fun i => n / p ^ i) = ((Finset.sum (Finset.Ico 1 b) fun i => k / p ^ i) + Finset.sum (Finset.Ico 1 b) fun i => (n - k) / p ^ i) + Finset.card (Finset.filter (fun i => p ^ i k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b))
theorem Nat.Prime.multiplicity_choose' {p : } {n : } {k : } {b : } (hp : Nat.Prime p) (hnb : Nat.log p (n + k) < b) :
multiplicity p (Nat.choose (n + k) k) = ↑(Finset.card (Finset.filter (fun i => p ^ i k % p ^ i + n % p ^ i) (Finset.Ico 1 b)))

The multiplicity of p in choose (n + k) k is the number of carries when k and n are added in base p. The set is expressed by filtering Ico 1 b where b is any bound greater than log p (n + k).

theorem Nat.Prime.multiplicity_choose {p : } {n : } {k : } {b : } (hp : Nat.Prime p) (hkn : k n) (hnb : Nat.log p n < b) :
multiplicity p (Nat.choose n k) = ↑(Finset.card (Finset.filter (fun i => p ^ i k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)))

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.

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

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 (Nat.choose (p ^ n) k) + multiplicity p k = n
theorem Nat.Prime.multiplicity_choose_prime_pow {p : } {n : } {k : } (hp : Nat.Prime p) (hkn : k p ^ n) (hk0 : k 0) :
theorem Nat.Prime.dvd_choose_pow {p : } {n : } {k : } (hp : Nat.Prime p) (hk : k 0) (hkp : k p ^ n) :
p Nat.choose (p ^ n) k
theorem Nat.Prime.dvd_choose_pow_iff {p : } {n : } {k : } (hp : Nat.Prime p) :
p Nat.choose (p ^ n) k k 0 k p ^ n