# mathlibdocumentation

data.nat.multiplicity

# 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 : } :
m 10 < nn b n = ((finset.filter (λ (i : ), m ^ i n) 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

theorem nat.prime.multiplicity_one {p : } :
1 = 0

theorem nat.prime.multiplicity_mul {p m n : } :
(m * n) = m + n

theorem nat.prime.multiplicity_pow {p m n : } :
(m ^ n) = n •ℕ m

theorem nat.prime.multiplicity_self {p : } :
p = 1

theorem nat.prime.multiplicity_pow_self {p n : } :
(p ^ n) = n

theorem nat.prime.multiplicity_factorial {p : } (hp : nat.prime p) {n b : } :
n b = ∑ (i : ) in b, n / p ^ i

The multiplicity of a prime in 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

theorem nat.prime.multiplicity_factorial_mul_succ {n p : } :
(p * (n + 1))! = (p * n)! + (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.

theorem nat.prime.multiplicity_factorial_mul {n p : } :
(p * n)! = + n

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

theorem nat.prime.pow_dvd_factorial_iff {p n r b : } :
n b(p ^ r n! r ∑ (i : ) in b, 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 at least n

theorem nat.prime.multiplicity_choose_aux {p n b k : } :
k n∑ (i : ) in b, n / p ^ i = ∑ (i : ) in b, k / p ^ i + ∑ (i : ) in b, (n - k) / p ^ i + (finset.filter (λ (i : ), p ^ i k % p ^ i + (n - k) % p ^ i) b)).card

theorem nat.prime.multiplicity_choose {p n k b : } :
k nn b (n.choose k) = ((finset.filter (λ (i : ), p ^ i k % p ^ i + (n - k) % p ^ i) 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.

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

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

theorem nat.prime.multiplicity_choose_prime_pow {p n k : } :
k p ^ n0 < k ((p ^ n).choose k) + k = n

theorem nat.multiplicity_two_factorial_lt {n : } :
n 0 < n