Basic lemmas on prime factorizations

Basic facts about factorization

Lemmas characterising when n.factorization p = 0

theorem Nat.factorization_eq_zero_of_lt {n : ℕ} {p : ℕ} (h : n < p) : n.factorization p = 0

@[simp]

theorem Nat.factorization_one_right (n : ℕ) : n.factorization 1 = 0

theorem Nat.dvd_of_factorization_pos {n : ℕ} {p : ℕ} (hn : n.factorization p ≠ 0) : p ∣ n

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

theorem Nat.prod_factorization_eq_prod_primeFactors {n : ℕ} {β : Type u_1} [CommMonoid β] (f : ℕ → ℕ → β) : n.factorization.prod f = ∏ p ∈ n.primeFactors, f p (n.factorization p)

A product over n.factorization can be written as a product over n.primeFactors;

theorem Nat.prod_primeFactors_prod_factorization {n : ℕ} {β : Type u_1} [CommMonoid β] (f : ℕ → β) : ∏ p ∈ n.primeFactors, f p = n.factorization.prod fun (p x : ℕ) => f p

A product over n.primeFactors can be written as a product over n.factorization;

Lemmas about factorizations of primes and prime powers

@[simp]

theorem Nat.Prime.factorization_self {p : ℕ} (hp : Nat.Prime p) : p.factorization p = 1

The multiplicity of prime p in p is 1

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.

theorem Nat.eq_factorization_iff {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf : ∀ p ∈ f.support, Nat.Prime p) : f = n.factorization ↔ (f.prod fun (x1 x2 : ℕ) => x1 ^ x2) = n

theorem Nat.factorizationEquiv_inv_apply {f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.support, Nat.Prime p) : ↑(Nat.factorizationEquiv.symm ⟨f, hf⟩) = f.prod fun (x1 x2 : ℕ) => x1 ^ x2

@[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_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) : p ^ n.factorization p ≤ n

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_ord_compl_eq_self (n : ℕ) (p : ℕ) : p ^ n.factorization 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) : n.factorization p < n

A crude upper bound on n.factorization p

theorem Nat.factorization_le_of_le_pow {n : ℕ} {p : ℕ} {b : ℕ} (hb : n ≤ p ^ b) : n.factorization p ≤ b

An upper bound on n.factorization p

theorem Nat.factorization_prime_le_iff_dvd {d : ℕ} {n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : (∀ (p : ℕ), Nat.Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n

theorem Nat.factorization_le_factorization_mul_left {a : ℕ} {b : ℕ} (hb : b ≠ 0) : a.factorization ≤ (a * b).factorization

theorem Nat.factorization_le_factorization_mul_right {a : ℕ} {b : ℕ} (ha : a ≠ 0) : b.factorization ≤ (a * b).factorization

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) : p ∣ n ↔ 1 ≤ n.factorization p

theorem Nat.exists_factorization_lt_of_lt {a : ℕ} {b : ℕ} (ha : a ≠ 0) (hab : a < b) : ∃ (p : ℕ), a.factorization p < b.factorization p

@[simp]

theorem Nat.factorization_div {d : ℕ} {n : ℕ} (h : d ∣ n) : (n / d).factorization = n.factorization - d.factorization

theorem Nat.dvd_ord_proj_of_dvd {n : ℕ} {p : ℕ} (hn : n ≠ 0) (pp : Nat.Prime p) (h : p ∣ n) : p ∣ p ^ n.factorization p

theorem Nat.not_dvd_ord_compl {n : ℕ} {p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) : ¬p ∣ n / p ^ n.factorization p

theorem Nat.coprime_ord_compl {n : ℕ} {p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) : p.Coprime (n / p ^ n.factorization p)

theorem Nat.factorization_ord_compl (n : ℕ) (p : ℕ) : (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

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.exists_eq_two_pow_mul_odd {n : ℕ} (hn : n ≠ 0) : ∃ (k : ℕ) (m : ℕ), Odd m ∧ n = 2 ^ k * m

Any nonzero natural number is the product of an odd part m and a power of two 2 ^ k.

theorem Nat.dvd_iff_div_factorization_eq_tsub {d : ℕ} {n : ℕ} (hd : d ≠ 0) (hdn : d ≤ n) : d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization

theorem Nat.ord_proj_dvd_ord_proj_of_dvd {a : ℕ} {b : ℕ} (hb0 : b ≠ 0) (hab : a ∣ b) (p : ℕ) : p ^ a.factorization p ∣ p ^ b.factorization 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_primeFactors_dvd (n : ℕ) : ∏ p ∈ n.primeFactors, p ∣ n

theorem Nat.factorization_gcd {a : ℕ} {b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) : (a.gcd b).factorization = a.factorization ⊓ b.factorization

theorem Nat.factorization_lcm {a : ℕ} {b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a.lcm b).factorization = a.factorization ⊔ b.factorization

@[simp]

theorem Nat.factorizationLCMLeft_zero_left (b : ℕ) : Nat.factorizationLCMLeft 0 b = 1

@[simp]

theorem Nat.factorizationLCMLeft_zero_right (a : ℕ) : a.factorizationLCMLeft 0 = 1

@[simp]

theorem Nat.factorizationLCRight_zero_left (b : ℕ) : Nat.factorizationLCMRight 0 b = 1

@[simp]

theorem Nat.factorizationLCMRight_zero_right (a : ℕ) : a.factorizationLCMRight 0 = 1

theorem Nat.factorizationLCMLeft_pos (a : ℕ) (b : ℕ) : 0 < a.factorizationLCMLeft b

theorem Nat.factorizationLCMRight_pos (a : ℕ) (b : ℕ) : 0 < a.factorizationLCMRight b

theorem Nat.coprime_factorizationLCMLeft_factorizationLCMRight (a : ℕ) (b : ℕ) : (a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)

theorem Nat.factorizationLCMLeft_mul_factorizationLCMRight {a : ℕ} {b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b

theorem Nat.factorizationLCMLeft_dvd_left (a : ℕ) (b : ℕ) : a.factorizationLCMLeft b ∣ a

theorem Nat.factorizationLCMRight_dvd_right (a : ℕ) (b : ℕ) : a.factorizationLCMRight b ∣ b

theorem Nat.prod_primeFactors_gcd_mul_prod_primeFactors_mul {β : Type u_1} [CommMonoid β] (m : ℕ) (n : ℕ) (f : ℕ → β) : (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

theorem Nat.sum_primeFactors_gcd_add_sum_primeFactors_mul {β : Type u_1} [AddCommMonoid β] (m : ℕ) (n : ℕ) (f : ℕ → β) : (m.gcd n).primeFactors.sum f + (m * n).primeFactors.sum f = m.primeFactors.sum f + n.primeFactors.sum f

theorem Nat.setOf_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 (fun (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 (fun (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 (fun (i : ℕ) => p ^ i ∣ n) (Finset.Ico 1 n) = Finset.filter (fun (i : ℕ) => p ^ i ∣ n) (Finset.Icc 1 b)

Factorization and coprimes

theorem Nat.factorization_eq_of_coprime_left {p : ℕ} {a : ℕ} {b : ℕ} (hab : a.Coprime b) (hpa : p ∈ a.primeFactorsList) : (a * b).factorization p = a.factorization p

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.primeFactorsList) : (a * b).factorization p = b.factorization p

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.

theorem Nat.eq_iff_prime_padicValNat_eq (a : ℕ) (b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : a = b ↔ ∀ (p : ℕ), Nat.Prime p → padicValNat p a = padicValNat p b

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

theorem Nat.prod_pow_prime_padicValNat (n : ℕ) (hn : n ≠ 0) (m : ℕ) (pr : n < m) : ∏ p ∈ Finset.filter Nat.Prime (Finset.range m), p ^ padicValNat p n = n

Lemmas about factorizations of particular functions

theorem Nat.card_multiples (n : ℕ) (p : ℕ) : (Finset.filter (fun (e : ℕ) => p ∣ e + 1) (Finset.range n)).card = n / p

Exactly n / p naturals in [1, n] are multiples of p. See Nat.card_multiples' for an alternative spelling of the statement.

theorem Nat.Ioc_filter_dvd_card_eq_div (n : ℕ) (p : ℕ) : (Finset.filter (fun (x : ℕ) => p ∣ x) (Finset.Ioc 0 n)).card = n / p

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

theorem Nat.card_multiples' (N : ℕ) (n : ℕ) : (Finset.filter (fun (k : ℕ) => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)).card = N / n

There are exactly ⌊N/n⌋ positive multiples of n that are ≤ N. See Nat.card_multiples for a "shifted-by-one" version.