mathlib documentation

data.nat.factorization.basic

Prime factorizations #

n.factorization is the finitely supported function ℕ →₀ ℕ mapping each prime factor of n to its multiplicity in n. For example, since 2000 = 2^4 * 5^3,

TODO #

n.factorization is the finitely supported function ℕ →₀ ℕ mapping each prime factor of n to its multiplicity in n.

Equations
theorem nat.factorization_def (n : ) {p : } (pp : nat.prime p) :
@[simp]

We can write both n.factorization p and n.factors.count p to represent the power of p in the factorization of n: we declare the former to be the simp-normal form.

theorem nat.multiplicity_eq_factorization {n p : } (pp : nat.prime p) (hn : n 0) :

Basic facts about factorization #

theorem nat.eq_of_factorization_eq {a b : } (ha : a 0) (hb : b 0) (h : (p : ), (a.factorization) p = (b.factorization) p) :
a = b

Every nonzero natural number has a unique prime factorization

@[simp]
@[simp]
@[simp]

The support of n.factorization is exactly n.factors.to_finset

theorem nat.pos_of_mem_factorization {n p : } (hp : p n.factorization.support) :
0 < p

Lemmas characterising when n.factorization p = 0 #

@[simp]
theorem nat.factorization_eq_zero_of_lt {n p : } (h : n < p) :
@[simp]
@[simp]
theorem nat.dvd_of_factorization_pos {n p : } (hn : (n.factorization) p 0) :
p n
theorem nat.prime.factorization_pos_of_dvd {n p : } (hp : nat.prime p) (hn : n 0) (h : p n) :
theorem nat.factorization_eq_zero_of_remainder {p r : } (i : ) (hr : ¬p r) :
((p * i + r).factorization) p = 0
theorem nat.factorization_eq_zero_iff_remainder {p r : } (i : ) (pp : nat.prime p) (hr0 : r 0) :
¬p r ((p * i + r).factorization) p = 0
theorem nat.factorization_eq_zero_iff' (n : ) :
n.factorization = 0 n = 0 n = 1

The only numbers with empty prime factorization are 0 and 1

Lemmas about factorizations of products and powers #

@[simp]
theorem nat.factorization_mul {a b : } (ha : a 0) (hb : b 0) :

For nonzero a and b, the power of p in a * b is the sum of the powers in a and b

theorem nat.prod_factorization_eq_prod_factors {n : } {β : Type u_1} [comm_monoid β] (f : β) :
n.factorization.prod (λ (p k : ), f p) = n.factors.to_finset.prod (λ (p : ), f p)

If a product over n.factorization doesn't use the multiplicities of the prime factors then it's equal to the corresponding product over n.factors.to_finset

theorem nat.factorization_prod {α : Type u_1} {S : finset α} {g : α } (hS : (x : α), x S g x 0) :
(S.prod g).factorization = S.sum (λ (x : α), (g x).factorization)

For any p : ℕ and any function g : α → ℕ that's non-zero on S : finset α, the power of p in S.prod g equals the sum over x ∈ S of the powers of p in g x. Generalises factorization_mul, which is the special case where S.card = 2 and g = id.

@[simp]
theorem nat.factorization_pow (n k : ) :

For any p, the power of p in n^k is k times the power in n

Lemmas about factorizations of primes and prime powers #

@[simp]

The only prime factor of prime p is p itself, with multiplicity 1

@[simp]
theorem nat.prime.factorization_self {p : } (hp : nat.prime p) :

The multiplicity of prime p in p is 1

theorem nat.prime.factorization_pow {p k : } (hp : nat.prime p) :

For prime p the only prime factor of p^k is p with multiplicity k

theorem nat.eq_pow_of_factorization_eq_single {n p k : } (hn : n 0) (h : n.factorization = finsupp.single p k) :
n = p ^ k

If the factorization of n contains just one number p then n is a power of p

theorem nat.prime.eq_of_factorization_pos {p q : } (hp : nat.prime p) (h : (p.factorization) q 0) :
p = q

The only prime factor of prime p is p itself.

Equivalence between ℕ+ and ℕ →₀ ℕ with support in the primes. #

Any finsupp f : ℕ →₀ ℕ whose support is in the primes is equal to the factorization of the product ∏ (a : ℕ) in f.support, a ^ f a.

theorem nat.eq_factorization_iff {n : } {f : →₀ } (hn : n 0) (hf : (p : ), p f.support nat.prime p) :

The equiv between ℕ+ and ℕ →₀ ℕ with support in the primes.

Equations

Generalisation of the "even part" and "odd part" of a natural number #

We introduce the notations ord_proj[p] n for the largest power of the prime p that divides n and ord_compl[p] n for the complementary part. The ord naming comes from the $p$-adic order/valuation of a number, and proj and compl are for the projection and complementary projection. The term n.factorization p is the $p$-adic order itself. For example, ord_proj[2] n is the even part of n and ord_compl[2] n is the odd part.

@[simp]
theorem nat.ord_proj_of_not_prime (n p : ) (hp : ¬nat.prime p) :
p ^ (n.factorization) p = 1
@[simp]
theorem nat.ord_compl_of_not_prime (n p : ) (hp : ¬nat.prime p) :
n / p ^ (n.factorization) p = n
theorem nat.ord_proj_dvd (n p : ) :
theorem nat.ord_compl_dvd (n p : ) :
n / p ^ (n.factorization) p n
theorem nat.ord_proj_pos (n p : ) :
0 < p ^ (n.factorization) p
theorem nat.ord_proj_le {n : } (p : ) (hn : n 0) :
theorem nat.ord_compl_pos {n : } (p : ) (hn : n 0) :
0 < n / p ^ (n.factorization) p
theorem nat.ord_compl_le (n p : ) :
n / p ^ (n.factorization) p n
theorem nat.ord_proj_mul {a b : } (p : ) (ha : a 0) (hb : b 0) :
p ^ ((a * b).factorization) p = p ^ (a.factorization) p * p ^ (b.factorization) p
theorem nat.ord_compl_mul (a b p : ) :
a * b / p ^ ((a * b).factorization) p = a / p ^ (a.factorization) p * (b / p ^ (b.factorization) p)

Factorization and divisibility #

theorem nat.factorization_lt {n : } (p : ) (hn : n 0) :

A crude upper bound on n.factorization p

theorem nat.factorization_le_of_le_pow {n p b : } (hb : n p ^ b) :

An upper bound on n.factorization p

theorem nat.factorization_le_iff_dvd {d n : } (hd : d 0) (hn : n 0) :
theorem nat.pow_succ_factorization_not_dvd {n p : } (hn : n 0) (hp : nat.prime p) :
¬p ^ ((n.factorization) p + 1) n
theorem nat.prime.pow_dvd_iff_le_factorization {p k n : } (pp : nat.prime p) (hn : n 0) :
p ^ k n k (n.factorization) p
theorem nat.prime.pow_dvd_iff_dvd_ord_proj {p k n : } (pp : nat.prime p) (hn : n 0) :
p ^ k n p ^ k p ^ (n.factorization) p
theorem nat.prime.dvd_iff_one_le_factorization {p n : } (pp : nat.prime p) (hn : n 0) :
theorem nat.exists_factorization_lt_of_lt {a b : } (ha : a 0) (hab : a < b) :
@[simp]
theorem nat.factorization_div {d n : } (h : d n) :
theorem nat.dvd_ord_proj_of_dvd {n p : } (hn : n 0) (pp : nat.prime p) (h : p n) :
theorem nat.not_dvd_ord_compl {n p : } (hp : nat.prime p) (hn : n 0) :
theorem nat.coprime_ord_compl {n p : } (hp : nat.prime p) (hn : n 0) :
p.coprime (n / p ^ (n.factorization) p)
theorem nat.dvd_ord_compl_of_dvd_not_dvd {p d n : } (hdn : d n) (hpd : ¬p d) :
d n / p ^ (n.factorization) p
theorem nat.exists_eq_pow_mul_and_not_dvd {n : } (hn : n 0) (p : ) (hp : p 1) :
(e n' : ), ¬p n' n = p ^ e * n'

If n is a nonzero natural number and p ≠ 1, then there are natural numbers e and n' such that n' is not divisible by p and n = p^e * n'.

theorem nat.dvd_iff_div_factorization_eq_tsub {d n : } (hd : d 0) (hdn : d n) :
theorem nat.ord_proj_dvd_ord_proj_of_dvd {a b : } (hb0 : b 0) (hab : a b) (p : ) :
theorem nat.ord_proj_dvd_ord_proj_iff_dvd {a b : } (ha0 : a 0) (hb0 : b 0) :
( (p : ), p ^ (a.factorization) p p ^ (b.factorization) p) a b
theorem nat.ord_compl_dvd_ord_compl_of_dvd {a b : } (hab : a b) (p : ) :
a / p ^ (a.factorization) p b / p ^ (b.factorization) p
theorem nat.ord_compl_dvd_ord_compl_iff_dvd (a b : ) :
( (p : ), a / p ^ (a.factorization) p b / p ^ (b.factorization) p) a b
theorem nat.dvd_iff_prime_pow_dvd_dvd (n d : ) :
d n (p k : ), nat.prime p p ^ k d p ^ k n
theorem nat.prod_prime_factors_dvd (n : ) :
n.factors.to_finset.prod (λ (p : ), p) n
theorem nat.factorization_gcd {a b : } (ha_pos : a 0) (hb_pos : b 0) :
theorem nat.set_of_pow_dvd_eq_Icc_factorization {n p : } (pp : nat.prime p) (hn : n 0) :
{i : | i 0 p ^ i n} = set.Icc 1 ((n.factorization) p)
theorem nat.Icc_factorization_eq_pow_dvd (n : ) {p : } (pp : nat.prime p) :
finset.Icc 1 ((n.factorization) p) = finset.filter (λ (i : ), p ^ i n) (finset.Ico 1 n)

The set of positive powers of prime p that divide n is exactly the set of positive natural numbers up to n.factorization p.

theorem nat.factorization_eq_card_pow_dvd (n : ) {p : } (pp : nat.prime p) :
(n.factorization) p = (finset.filter (λ (i : ), p ^ i n) (finset.Ico 1 n)).card
theorem nat.Ico_filter_pow_dvd_eq {n p b : } (pp : nat.prime p) (hn : n 0) (hb : n p ^ b) :
finset.filter (λ (i : ), p ^ i n) (finset.Ico 1 n) = finset.filter (λ (i : ), p ^ i n) (finset.Icc 1 b)

Factorization and coprimes #

For coprime a and b, the power of p in a * b is the sum of the powers in a and b

For coprime a and b, the power of p in a * b is the sum of the powers in a and b

theorem nat.factorization_eq_of_coprime_left {p a b : } (hab : a.coprime b) (hpa : p a.factors) :

If p is a prime factor of a then the power of p in a is the same that in a * b, for any b coprime to a.

theorem nat.factorization_eq_of_coprime_right {p a b : } (hab : a.coprime b) (hpb : p b.factors) :

If p is a prime factor of b then the power of p in b is the same that in a * b, for any a coprime to b.

The prime factorizations of coprime a and b are disjoint

For coprime a and b the prime factorization a * b is the union of those of a and b

Induction principles involving factorizations #

def nat.rec_on_prime_pow {P : Sort u_1} (h0 : P 0) (h1 : P 1) (h : Π (a p n : ), nat.prime p ¬p a 0 < n P a P (p ^ n * a)) (a : ) :
P a

Given P 0, P 1 and a way to extend P a to P (p ^ n * a) for prime p not dividing a, we can define P for all natural numbers.

Equations
def nat.rec_on_pos_prime_pos_coprime {P : Sort u_1} (hp : Π (p n : ), nat.prime p 0 < n P (p ^ n)) (h0 : P 0) (h1 : P 1) (h : Π (a b : ), 1 < a 1 < b a.coprime b P a P b P (a * b)) (a : ) :
P a

Given P 0, P 1, and P (p ^ n) for positive prime powers, and a way to extend P a and P b to P (a * b) when a, b are positive coprime, we can define P for all natural numbers.

Equations
def nat.rec_on_prime_coprime {P : Sort u_1} (h0 : P 0) (hp : Π (p n : ), nat.prime p P (p ^ n)) (h : Π (a b : ), 1 < a 1 < b a.coprime b P a P b P (a * b)) (a : ) :
P a

Given P 0, P (p ^ n) for all prime powers, and a way to extend P a and P b to P (a * b) when a, b are positive coprime, we can define P for all natural numbers.

Equations
def nat.rec_on_mul {P : Sort u_1} (h0 : P 0) (h1 : P 1) (hp : Π (p : ), nat.prime p P p) (h : Π (a b : ), P a P b P (a * b)) (a : ) :
P a

Given P 0, P 1, P p for all primes, and a way to extend P a and P b to P (a * b), we can define P for all natural numbers.

Equations
theorem nat.multiplicative_factorization {β : Type u_1} [comm_monoid β] (f : β) (h_mult : (x y : ), x.coprime y f (x * y) = f x * f y) (hf : f 1 = 1) {n : } :
n 0 f n = n.factorization.prod (λ (p k : ), f (p ^ k))

For any multiplicative function f with f 1 = 1 and any n ≠ 0, we can evaluate f n by evaluating f at p ^ k over the factorization of n

theorem nat.multiplicative_factorization' {β : Type u_1} [comm_monoid β] (f : β) (h_mult : (x y : ), x.coprime y f (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) {n : } :
f n = n.factorization.prod (λ (p k : ), f (p ^ k))

For any multiplicative function f with f 1 = 1 and f 0 = 1, we can evaluate f n by evaluating f at p ^ k over the factorization of n

theorem nat.eq_iff_prime_padic_val_nat_eq (a b : ) (ha : a 0) (hb : b 0) :

Two positive naturals are equal if their prime padic valuations are equal

theorem nat.prod_pow_prime_padic_val_nat (n : ) (hn : n 0) (m : ) (pr : n < m) :

Lemmas about factorizations of particular functions #

theorem nat.card_multiples (n p : ) :
(finset.filter (λ (e : ), p e + 1) (finset.range n)).card = n / p

Exactly n / p naturals in [1, n] are multiples of p.

theorem nat.Ioc_filter_dvd_card_eq_div (n p : ) :
(finset.filter (λ (x : ), p x) (finset.Ioc 0 n)).card = n / p

Exactly n / p naturals in (0, n] are multiples of p.