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
Instances For
    @[simp]
    @[simp]
    theorem Nat.pos_of_mem_factors {n : } {p : } (h : p Nat.factors n) :
    0 < p
    theorem Nat.prod_factors {n : } :
    n 0List.prod (Nat.factors n) = n
    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) :
    @[simp]
    theorem Nat.mem_factors' {n : } {p : } :
    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₂ : pl, Nat.Prime p) :

    Fundamental theorem of arithmetic

    theorem Nat.Prime.factors_pow {p : } (hp : Nat.Prime p) (n : ) :
    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_right {n : } {k : } (h : k 0) :
    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