Documentation

Mathlib.Data.Nat.Factors

Prime numbers #

This file deals with the factors of natural numbers.

Important declarations #

@[irreducible]

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

Equations
Instances For
    @[deprecated Nat.primeFactorsList]

    Alias of Nat.primeFactorsList.


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

    Equations
    Instances For
      @[irreducible]
      theorem Nat.prime_of_mem_primeFactorsList {n : } {p : } :
      p n.primeFactorsListNat.Prime p
      theorem Nat.pos_of_mem_primeFactorsList {n : } {p : } (h : p n.primeFactorsList) :
      0 < p
      @[irreducible]
      theorem Nat.prod_primeFactorsList {n : } :
      n 0n.primeFactorsList.prod = n
      theorem Nat.primeFactorsList_prime {p : } (hp : Nat.Prime p) :
      p.primeFactorsList = [p]
      @[irreducible]
      theorem Nat.primeFactorsList_chain {n : } {a : } :
      (∀ (p : ), Nat.Prime pp na p)List.Chain (fun (x1 x2 : ) => x1 x2) a n.primeFactorsList
      theorem Nat.primeFactorsList_chain_2 (n : ) :
      List.Chain (fun (x1 x2 : ) => x1 x2) 2 n.primeFactorsList
      theorem Nat.primeFactorsList_chain' (n : ) :
      List.Chain' (fun (x1 x2 : ) => x1 x2) n.primeFactorsList
      theorem Nat.primeFactorsList_sorted (n : ) :
      List.Sorted (fun (x1 x2 : ) => x1 x2) n.primeFactorsList
      theorem Nat.primeFactorsList_add_two (n : ) :
      (n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList

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

      @[simp]
      theorem Nat.primeFactorsList_eq_nil (n : ) :
      n.primeFactorsList = [] n = 0 n = 1
      theorem Nat.eq_of_perm_primeFactorsList {a : } {b : } (ha : a 0) (hb : b 0) (h : a.primeFactorsList.Perm b.primeFactorsList) :
      a = b
      theorem Nat.mem_primeFactorsList_iff_dvd {n : } {p : } (hn : n 0) (hp : Nat.Prime p) :
      p n.primeFactorsList p n
      theorem Nat.dvd_of_mem_primeFactorsList {n : } {p : } (h : p n.primeFactorsList) :
      p n
      theorem Nat.mem_primeFactorsList {n : } {p : } (hn : n 0) :
      p n.primeFactorsList Nat.Prime p p n
      @[simp]
      theorem Nat.mem_primeFactorsList' {n : } {p : } :
      p n.primeFactorsList Nat.Prime p p n n 0
      theorem Nat.le_of_mem_primeFactorsList {n : } {p : } (h : p n.primeFactorsList) :
      p n
      theorem Nat.primeFactorsList_unique {n : } {l : List } (h₁ : l.prod = n) (h₂ : pl, Nat.Prime p) :
      l.Perm n.primeFactorsList

      Fundamental theorem of arithmetic

      theorem Nat.Prime.primeFactorsList_pow {p : } (hp : Nat.Prime p) (n : ) :
      (p ^ n).primeFactorsList = 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.primeFactorsList.length
      theorem Nat.perm_primeFactorsList_mul {a : } {b : } (ha : a 0) (hb : b 0) :
      (a * b).primeFactorsList.Perm (a.primeFactorsList ++ b.primeFactorsList)

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

      theorem Nat.perm_primeFactorsList_mul_of_coprime {a : } {b : } (hab : a.Coprime b) :
      (a * b).primeFactorsList.Perm (a.primeFactorsList ++ b.primeFactorsList)

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

      theorem Nat.primeFactorsList_sublist_right {n : } {k : } (h : k 0) :
      n.primeFactorsList.Sublist (n * k).primeFactorsList
      theorem Nat.primeFactorsList_sublist_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
      n.primeFactorsList.Sublist k.primeFactorsList
      theorem Nat.primeFactorsList_subset_right {n : } {k : } (h : k 0) :
      n.primeFactorsList (n * k).primeFactorsList
      theorem Nat.primeFactorsList_subset_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
      n.primeFactorsList k.primeFactorsList
      theorem Nat.dvd_of_primeFactorsList_subperm {a : } {b : } (ha : a 0) (h : a.primeFactorsList.Subperm b.primeFactorsList) :
      a b
      theorem Nat.replicate_subperm_primeFactorsList_iff {a : } {b : } {n : } (ha : Nat.Prime a) (hb : b 0) :
      (List.replicate n a).Subperm b.primeFactorsList a ^ n b
      theorem Nat.mem_primeFactorsList_mul {a : } {b : } (ha : a 0) (hb : b 0) {p : } :
      p (a * b).primeFactorsList p a.primeFactorsList p b.primeFactorsList
      theorem Nat.coprime_primeFactorsList_disjoint {a : } {b : } (hab : a.Coprime b) :
      a.primeFactorsList.Disjoint b.primeFactorsList

      The sets of factors of coprime a and b are disjoint

      theorem Nat.mem_primeFactorsList_mul_of_coprime {a : } {b : } (hab : a.Coprime b) (p : ) :
      p (a * b).primeFactorsList p a.primeFactorsList b.primeFactorsList
      theorem Nat.mem_primeFactorsList_mul_left {p : } {a : } {b : } (hpa : p a.primeFactorsList) (hb : b 0) :
      p (a * b).primeFactorsList

      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_primeFactorsList_mul_right {p : } {a : } {b : } (hpb : p b.primeFactorsList) (ha : a 0) :
      p (a * b).primeFactorsList

      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