mathlib3 documentation

data.nat.factors

Prime numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file deals with the factors of natural numbers.

Important declarations #

source
def nat.factors  :
ℕ → list ℕ

factors n is the prime factorization of n, listed in increasing order.

Equations
source
@[simp]
theorem nat.factors_zero  :
0.factors = list.nil
source
@[simp]
theorem nat.factors_one  :
1.factors = list.nil
source
theorem nat.prime_of_mem_factors {n p : ℕ} :
p ∈ n.factors → nat.prime p
source
theorem nat.pos_of_mem_factors {n p : ℕ} (h : p ∈ n.factors) :
0 < p
source
theorem nat.prod_factors {n : ℕ} :
n ≠ 0 → n.factors.prod = n
source
theorem nat.factors_prime {p : ℕ} (hp : nat.prime p) :
p.factors = [p]
source
theorem nat.factors_chain {n a : ℕ} :
(∀ (p : ℕ), nat.prime p → p ∣ n → a ≤ p) → list.chain has_le.le a n.factors
source
theorem nat.factors_chain_2 (n : ℕ) :
list.chain has_le.le 2 n.factors
source
theorem nat.factors_chain' (n : ℕ) :
list.chain' has_le.le n.factors
source
theorem nat.factors_sorted (n : ℕ) :
list.sorted has_le.le n.factors
source
theorem nat.factors_add_two (n : ℕ) :
(n + 2).factors = (n + 2).min_fac :: ((n + 2) / (n + 2).min_fac).factors

factors can be constructed inductively by extracting min_fac, for sufficiently large n.

source
@[simp]
theorem nat.factors_eq_nil (n : ℕ) :
n.factors = list.nil ↔ n = 0 ∨ n = 1
source
theorem nat.eq_of_perm_factors {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : a.factors ~ b.factors) :
a = b
source
theorem nat.mem_factors_iff_dvd {n p : ℕ} (hn : n ≠ 0) (hp : nat.prime p) :
p ∈ n.factors ↔ p ∣ n
source
theorem nat.dvd_of_mem_factors {n p : ℕ} (h : p ∈ n.factors) :
p ∣ n
source
theorem nat.mem_factors {n p : ℕ} (hn : n ≠ 0) :
p ∈ n.factors ↔ nat.prime p ∧ p ∣ n
source
theorem nat.le_of_mem_factors {n p : ℕ} (h : p ∈ n.factors) :
p ≤ n
source
theorem nat.factors_unique {n : ℕ} {l : list ℕ} (h₁ : l.prod = n) (h₂ : ∀ (p : ℕ), p ∈ l → nat.prime p) :
l ~ n.factors

Fundamental theorem of arithmetic

source
theorem nat.prime.factors_pow {p : ℕ} (hp : nat.prime p) (n : ℕ) :
(p ^ n).factors = list.replicate n p
source
theorem nat.eq_prime_pow_of_unique_prime_dvd {n p : ℕ} (hpos : n ≠ 0) (h : ∀ {d : ℕ}, nat.prime d → d ∣ n → d = p) :
n = p ^ n.factors.length
source
theorem nat.perm_factors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a * b).factors ~ a.factors ++ b.factors

For positive a and b, the prime factors of a * b are the union of those of a and b

source
theorem nat.perm_factors_mul_of_coprime {a b : ℕ} (hab : a.coprime b) :
(a * b).factors ~ a.factors ++ b.factors

For coprime a and b, the prime factors of a * b are the union of those of a and b

source
theorem nat.factors_sublist_right {n k : ℕ} (h : k ≠ 0) :
n.factors <+ (n * k).factors
source
theorem nat.factors_sublist_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) :
n.factors <+ k.factors
source
theorem nat.factors_subset_right {n k : ℕ} (h : k ≠ 0) :
n.factors ⊆ (n * k).factors
source
theorem nat.factors_subset_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) :
n.factors ⊆ k.factors
source
theorem nat.dvd_of_factors_subperm {a b : ℕ} (ha : a ≠ 0) (h : a.factors <+~ b.factors) :
a ∣ b
source
theorem nat.mem_factors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) {p : ℕ} :
p ∈ (a * b).factors ↔ p ∈ a.factors ∨ p ∈ b.factors
source
theorem nat.coprime_factors_disjoint {a b : ℕ} (hab : a.coprime b) :
a.factors.disjoint b.factors

The sets of factors of coprime a and b are disjoint

source
theorem nat.mem_factors_mul_of_coprime {a b : ℕ} (hab : a.coprime b) (p : ℕ) :
p ∈ (a * b).factors ↔ p ∈ a.factors ∪ b.factors
source
theorem nat.mem_factors_mul_left {p a b : ℕ} (hpa : p ∈ a.factors) (hb : b ≠ 0) :
p ∈ (a * b).factors

If p is a prime factor of a then p is also a prime factor of a * b for any b > 0

source
theorem nat.mem_factors_mul_right {p a b : ℕ} (hpb : p ∈ b.factors) (ha : a ≠ 0) :
p ∈ (a * b).factors

If p is a prime factor of b then p is also a prime factor of a * b for any a > 0

source
theorem nat.eq_two_pow_or_exists_odd_prime_and_dvd (n : ℕ) :
(∃ (k : ℕ), n = 2 ^ k) ∨ ∃ (p : ℕ), nat.prime p ∧ p ∣ n ∧ odd p