mathlib3 documentation

data.nat.multiplicity

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 #

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.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.

theorem nat.prime.multiplicity_one {p : } (hp : nat.prime p) :
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_self {p : } (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 < 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.

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 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

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
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.

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) :
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 _)
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
theorem nat.prime.dvd_choose_pow_iff {p n k : } (hp : nat.prime p) :
p (p ^ n).choose k k 0 k p ^ n