Documentation

Mathlib.Data.Nat.Factors

Prime numbers #

This file deals with the factors of natural numbers.

Important declarations #

@[irreducible]

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

Equations
Instances For
    @[simp]
    @[simp]
    @[simp]
    @[irreducible]
    theorem Nat.prime_of_mem_factors {n : } {p : } (h : p n.factors) :
    theorem Nat.pos_of_mem_factors {n : } {p : } (h : p n.factors) :
    0 < p
    @[irreducible]
    theorem Nat.prod_factors {n : } :
    n 0n.factors.prod = n
    theorem Nat.factors_prime {p : } (hp : Nat.Prime p) :
    p.factors = [p]
    @[irreducible]
    theorem Nat.factors_chain {n : } {a : } :
    (∀ (p : ), Nat.Prime pp na p)List.Chain (fun (x x_1 : ) => x x_1) a n.factors
    theorem Nat.factors_chain_2 (n : ) :
    List.Chain (fun (x x_1 : ) => x x_1) 2 n.factors
    theorem Nat.factors_chain' (n : ) :
    List.Chain' (fun (x x_1 : ) => x x_1) n.factors
    theorem Nat.factors_sorted (n : ) :
    List.Sorted (fun (x x_1 : ) => x x_1) n.factors
    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.

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

    Fundamental theorem of arithmetic

    theorem Nat.Prime.factors_pow {p : } (hp : Nat.Prime p) (n : ) :
    (p ^ n).factors = List.replicate n p
    theorem Nat.eq_prime_pow_of_unique_prime_dvd {n : } {p : } (hpos : n 0) (h : ∀ {d : }, Nat.Prime dd nd = p) :
    n = p ^ n.factors.length
    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

    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

    theorem Nat.factors_sublist_right {n : } {k : } (h : k 0) :
    n.factors.Sublist (n * k).factors
    theorem Nat.factors_sublist_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
    n.factors.Sublist k.factors
    theorem Nat.factors_subset_right {n : } {k : } (h : k 0) :
    n.factors (n * k).factors
    theorem Nat.factors_subset_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
    n.factors k.factors
    theorem Nat.dvd_of_factors_subperm {a : } {b : } (ha : a 0) (h : a.factors.Subperm b.factors) :
    a b
    theorem Nat.replicate_subperm_factors_iff {a : } {b : } {n : } (ha : Nat.Prime a) (hb : b 0) :
    (List.replicate n a).Subperm b.factors a ^ n b
    theorem Nat.mem_factors_mul {a : } {b : } (ha : a 0) (hb : b 0) {p : } :
    p (a * b).factors p a.factors p b.factors
    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

    theorem Nat.mem_factors_mul_of_coprime {a : } {b : } (hab : a.Coprime b) (p : ) :
    p (a * b).factors p a.factors b.factors
    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

    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

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