Documentation

Mathlib.Data.Nat.Factors

Prime numbers #

This file deals with the factors of natural numbers.

Important declarations #

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

Equations
@[simp]
theorem Nat.pos_of_mem_factors {n : } {p : } (h : p Nat.factors n) :
0 < p
theorem Nat.factors_prime {p : } (hp : Nat.Prime p) :
theorem Nat.factors_chain {n : } {a : } :
(∀ (p : ), Nat.Prime pp na p) → List.Chain (fun x x_1 => x x_1) a (Nat.factors n)
theorem Nat.factors_chain_2 (n : ) :
List.Chain (fun x x_1 => x x_1) 2 (Nat.factors n)
theorem Nat.factors_chain' (n : ) :
List.Chain' (fun x x_1 => x x_1) (Nat.factors n)
theorem Nat.factors_sorted (n : ) :
List.Sorted (fun x x_1 => x x_1) (Nat.factors n)
theorem Nat.factors_add_two (n : ) :
Nat.factors (n + 2) = Nat.minFac (n + 2) :: Nat.factors ((n + 2) / Nat.minFac (n + 2))

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

@[simp]
theorem Nat.factors_eq_nil (n : ) :
Nat.factors n = [] n = 0 n = 1
theorem Nat.eq_of_perm_factors {a : } {b : } (ha : a 0) (hb : b 0) (h : Nat.factors a ~ Nat.factors b) :
a = b
theorem Nat.mem_factors_iff_dvd {n : } {p : } (hn : n 0) (hp : Nat.Prime p) :
theorem Nat.dvd_of_mem_factors {n : } {p : } (h : p Nat.factors n) :
p n
theorem Nat.mem_factors {n : } {p : } (hn : n 0) :
theorem Nat.le_of_mem_factors {n : } {p : } (h : p Nat.factors n) :
p n
theorem Nat.factors_unique {n : } {l : List } (h₁ : List.prod l = n) (h₂ : ∀ (p : ), p lNat.Prime p) :

Fundamental theorem of arithmetic

theorem Nat.eq_prime_pow_of_unique_prime_dvd {n : } {p : } (hpos : n 0) (h : ∀ {d : }, Nat.Prime dd nd = p) :
theorem Nat.perm_factors_mul {a : } {b : } (ha : a 0) (hb : b 0) :

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

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

theorem Nat.factors_sublist_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
theorem Nat.factors_subset_right {n : } {k : } (h : k 0) :
theorem Nat.factors_subset_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
theorem Nat.dvd_of_factors_subperm {a : } {b : } (ha : a 0) (h : Nat.factors a <+~ Nat.factors b) :
a b
theorem Nat.mem_factors_mul {a : } {b : } (ha : a 0) (hb : b 0) {p : } :

The sets of factors of coprime a and b are disjoint

theorem Nat.mem_factors_mul_left {p : } {a : } {b : } (hpa : p Nat.factors a) (hb : b 0) :
p Nat.factors (a * b)

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

theorem Nat.mem_factors_mul_right {p : } {a : } {b : } (hpb : p Nat.factors b) (ha : a 0) :
p Nat.factors (a * b)

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

theorem Nat.eq_two_pow_or_exists_odd_prime_and_dvd (n : ) :
(k, n = 2 ^ k) p, Nat.Prime p p n Odd p