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

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 : 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.factorization_prod_apply {α : Type u_1} {p : ℕ} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) : (S.prod g).factorization p = ∑ x ∈ S, (g x).factorization p

Modified version of factorization_prod that accounts for inputs.

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

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

The multiplicity of prime p in p is 1

theorem Nat.factorization_pow_self {p n : ℕ} (hp : Prime p) : (p ^ n).factorization p = n

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 : 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, Prime p) : f = n.factorization ↔ (f.prod fun (x1 x2 : ℕ) => x1 ^ x2) = n

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

theorem Nat.ordProj_of_not_prime (n p : ℕ) (hp : ¬Prime p) : p ^ n.factorization p = 1

theorem Nat.ordCompl_of_not_prime (n p : ℕ) (hp : ¬Prime p) : n / p ^ n.factorization p = n

theorem Nat.ordCompl_dvd (n p : ℕ) : n / p ^ n.factorization p ∣ n

theorem Nat.ordProj_pos (n p : ℕ) : 0 < p ^ n.factorization p

theorem Nat.ordProj_le {n : ℕ} (p : ℕ) (hn : n ≠ 0) : p ^ n.factorization p ≤ n

theorem Nat.ordCompl_pos {n : ℕ} (p : ℕ) (hn : n ≠ 0) : 0 < n / p ^ n.factorization p

theorem Nat.ordCompl_le (n p : ℕ) : n / p ^ n.factorization p ≤ n

theorem Nat.ordProj_mul_ordCompl_eq_self (n p : ℕ) : p ^ n.factorization p * (n / p ^ n.factorization p) = n

theorem Nat.ordProj_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.ordCompl_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 : ℕ), 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 : Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ k ≤ n.factorization p

theorem Nat.Prime.pow_dvd_iff_dvd_ordProj {p k n : ℕ} (pp : 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 : 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_ordProj_of_dvd {n p : ℕ} (hn : n ≠ 0) (pp : Prime p) (h : p ∣ n) : p ∣ p ^ n.factorization p

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

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

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

theorem Nat.ordProj_self_pow {p k : ℕ} (hp : Prime p) : p ^ (p ^ k).factorization p = p ^ k

theorem Nat.ordCompl_self_pow {p k : ℕ} (hp : Prime p) : p ^ k / p ^ (p ^ k).factorization p = 1

theorem Nat.ordCompl_self_pow_mul (n k : ℕ) {p : ℕ} (hp : Prime p) : p ^ k * n / p ^ (p ^ k * n).factorization p = n / p ^ n.factorization p

theorem Nat.ordCompl_eq_self_iff_zero_or_not_dvd (n : ℕ) {p : ℕ} (hp : Prime p) : n / p ^ n.factorization p = n ↔ n = 0 ∨ ¬p ∣ n

theorem Nat.dvd_ordCompl_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.ordProj_dvd_ordProj_of_dvd {a b : ℕ} (hb0 : b ≠ 0) (hab : a ∣ b) (p : ℕ) : p ^ a.factorization p ∣ p ^ b.factorization p

theorem Nat.ordCompl_dvd_ordCompl_of_dvd {a b : ℕ} (hab : a ∣ b) (p : ℕ) : a / p ^ a.factorization p ∣ b / p ^ b.factorization p

theorem Nat.ordCompl_dvd_ordCompl_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 : ℕ), 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

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 : 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 : Prime p) : Finset.Icc 1 (n.factorization p) = {i ∈ Finset.Ico 1 n | p ^ i ∣ 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 : Prime p) : n.factorization p = {i ∈ Finset.Ico 1 n | p ^ i ∣ n}.card

theorem Nat.Ico_filter_pow_dvd_eq {n p b : ℕ} (pp : Prime p) (hn : n ≠ 0) (hb : n ≤ p ^ b) : {i ∈ Finset.Ico 1 n | p ^ i ∣ n} = {i ∈ Finset.Icc 1 b | p ^ i ∣ n}

theorem Nat.Ico_pow_dvd_eq_Ico_of_lt {n p b : ℕ} (pp : Prime p) (hn : n ≠ 0) (hb : n < p ^ b) : {i ∈ Finset.Ico 1 n | p ^ i ∣ n} = {i ∈ Finset.Ico 1 b | p ^ i ∣ n}

theorem Nat.factorization_eq_card_pow_dvd_of_lt {b m n : ℕ} (hm : Prime m) (hn : 0 < n) (hb : n < m ^ b) : n.factorization m = {i ∈ Finset.Ico 1 b | m ^ i ∣ n}.card

The factorization of m in n is the number of positive natural numbers i such that m ^ i divides n. Note m is prime. This set is expressed by filtering Ico 1 b where b is any bound greater than log m n.

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 : ℕ), 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.range m with Prime p, p ^ padicValNat p n = n

theorem Nat.prod_pow_primeFactors_factorization {n : ℕ} (hn : n ≠ 0) : n = ∏ p : ↥n.primeFactors, ↑p ^ n.factorization ↑p

theorem Nat.pairwise_coprime_pow_primeFactors_factorization {n : ℕ} : Pairwise (Function.onFun Coprime fun (p : ↥n.primeFactors) => ↑p ^ n.factorization ↑p)

Lemmas about factorizations of particular functions

theorem Nat.card_multiples (n p : ℕ) : {e ∈ Finset.range n | p ∣ e + 1}.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 : ℕ) : {x ∈ Finset.Ioc 0 n | p ∣ x}.card = n / p

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

theorem Nat.card_multiples' (N n : ℕ) : {k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}.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.

theorem Nat.exists_eq_pow_of_exponent_coprime_of_pow_eq_pow {a b m n : ℕ} (hmn : m.Coprime n) (h : a ^ m = b ^ n) : ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m

theorem Nat.exists_eq_pow_of_pow_eq_pow {a b m n : ℕ} (hmn : m ≠ 0 ∨ n ≠ 0) (h : a ^ m = b ^ n) : ∃ (c : ℕ), a = c ^ (n / m.gcd n) ∧ b = c ^ (m / m.gcd n)