Documentation

Mathlib.Data.Nat.Factors

Prime numbers #

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
Instances For
    source
    @[simp]
    theorem Nat.factors_zero :
    Nat.factors 0 = []
    source
    @[simp]
    theorem Nat.factors_one :
    Nat.factors 1 = []
    source
    @[simp]
    theorem Nat.factors_two :
    Nat.factors 2 = [2]
    source
    theorem Nat.prime_of_mem_factors {n : ℕ} {p : ℕ} (h : p ∈ n.factors) :
    p.Prime
    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 : p.Prime) :
    p.factors = [p]
    source
    theorem Nat.factors_chain {n : ℕ} {a : ℕ} :
    (∀ (p : ℕ), p.Prime → p ∣ n → a ≤ p) → List.Chain (fun (x x_1 : ℕ) => x ≤ x_1) a n.factors
    source
    theorem Nat.factors_chain_2 (n : ℕ) :
    List.Chain (fun (x x_1 : ℕ) => x ≤ x_1) 2 n.factors
    source
    theorem Nat.factors_chain' (n : ℕ) :
    List.Chain' (fun (x x_1 : ℕ) => x ≤ x_1) n.factors
    source
    theorem Nat.factors_sorted (n : ℕ) :
    List.Sorted (fun (x x_1 : ℕ) => x ≤ x_1) n.factors
    source
    theorem Nat.factors_add_two (n : ℕ) :
    (n + 2).factors = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).factors

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

    source
    @[simp]
    theorem Nat.factors_eq_nil (n : ℕ) :
    n.factors = [] ↔ n = 0 ∨ n = 1
    source
    theorem Nat.eq_of_perm_factors {a : ℕ} {b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : a.factors.Perm b.factors) :
    a = b
    source
    theorem Nat.mem_factors_iff_dvd {n : ℕ} {p : ℕ} (hn : n ≠ 0) (hp : p.Prime) :
    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 ↔ p.Prime ∧ p ∣ n
    source
    @[simp]
    theorem Nat.mem_factors' {n : ℕ} {p : ℕ} :
    p ∈ n.factors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0
    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 ∈ l, p.Prime) :
    l.Perm n.factors

    Fundamental theorem of arithmetic

    source
    theorem Nat.Prime.factors_pow {p : ℕ} (hp : p.Prime) (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 : ℕ}, d.Prime → 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.Perm (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.Perm (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.Sublist (n * k).factors
    source
    theorem Nat.factors_sublist_of_dvd {n : ℕ} {k : ℕ} (h : n ∣ k) (h' : k ≠ 0) :
    n.factors.Sublist 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.Subperm b.factors) :
    a ∣ b
    source
    theorem Nat.replicate_subperm_factors_iff {a : ℕ} {b : ℕ} {n : ℕ} (ha : a.Prime) (hb : b ≠ 0) :
    (List.replicate n a).Subperm b.factors ↔ a ^ n ∣ 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 : ℕ), p.Prime ∧ p ∣ n ∧ Odd p
    source
    theorem Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt {n : ℕ} (n2 : 2 < n) :
    4 ∣ n ∨ ∃ (p : ℕ), p.Prime ∧ p ∣ n ∧ Odd p