Documentation

Mathlib.Data.Nat.Prime

Prime numbers #

This file deals with prime numbers: natural numbers p ≥ 2 whose only divisors are p and 1.

Important declarations #

def Nat.Prime (p : ) :

Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1.

Equations
Instances For
    theorem Nat.Prime.ne_zero {n : } (h : Nat.Prime n) :
    n 0
    theorem Nat.Prime.pos {p : } (pp : Nat.Prime p) :
    0 < p
    theorem Nat.Prime.two_le {p : } :
    Nat.Prime p2 p
    theorem Nat.Prime.one_lt {p : } :
    Nat.Prime p1 < p
    theorem Nat.Prime.one_le {p : } (hp : Nat.Prime p) :
    1 p
    instance Nat.Prime.one_lt' (p : ) [hp : Fact (Nat.Prime p)] :
    Fact (1 < p)
    Equations
    theorem Nat.Prime.ne_one {p : } (hp : Nat.Prime p) :
    p 1
    theorem Nat.Prime.eq_one_or_self_of_dvd {p : } (pp : Nat.Prime p) (m : ) (hm : m p) :
    m = 1 m = p
    theorem Nat.prime_def_lt'' {p : } :
    Nat.Prime p 2 p ∀ (m : ), m pm = 1 m = p
    theorem Nat.prime_def_lt {p : } :
    Nat.Prime p 2 p m < p, m pm = 1
    theorem Nat.prime_def_lt' {p : } :
    Nat.Prime p 2 p ∀ (m : ), 2 mm < p¬m p
    theorem Nat.prime_def_le_sqrt {p : } :
    Nat.Prime p 2 p ∀ (m : ), 2 mm Nat.sqrt p¬m p
    theorem Nat.prime_of_coprime (n : ) (h1 : 1 < n) (h : m < n, m 0Nat.Coprime n m) :

    This instance is slower than the instance decidablePrime defined below, but has the advantage that it works in the kernel for small values.

    If you need to prove that a particular number is prime, in any case you should not use by decide, but rather by norm_num, which is much faster.

    Equations
    Instances For
      theorem Nat.Prime.five_le_of_ne_two_of_ne_three {p : } (hp : Nat.Prime p) (h_two : p 2) (h_three : p 3) :
      5 p
      theorem Nat.Prime.pred_pos {p : } (pp : Nat.Prime p) :
      theorem Nat.dvd_prime {p : } {m : } (pp : Nat.Prime p) :
      m p m = 1 m = p
      theorem Nat.dvd_prime_two_le {p : } {m : } (pp : Nat.Prime p) (H : 2 m) :
      m p m = p
      theorem Nat.prime_dvd_prime_iff_eq {p : } {q : } (pp : Nat.Prime p) (qp : Nat.Prime q) :
      p q p = q
      theorem Nat.Prime.not_dvd_one {p : } (pp : Nat.Prime p) :
      ¬p 1
      theorem Nat.prime_mul_iff {a : } {b : } :
      theorem Nat.not_prime_mul {a : } {b : } (a1 : a 1) (b1 : b 1) :
      theorem Nat.not_prime_mul' {a : } {b : } {n : } (h : a * b = n) (h₁ : a 1) (h₂ : b 1) :
      theorem Nat.Prime.dvd_iff_eq {p : } {a : } (hp : Nat.Prime p) (a1 : a 1) :
      a p p = a
      theorem Nat.minFac_lemma (n : ) (k : ) (h : ¬n < k * k) :
      Nat.sqrt n - k < Nat.sqrt n + 2 - k
      def Nat.minFacAux (n : ) :

      If n < k * k, then minFacAux n k = n, if k | n, then minFacAux n k = k. Otherwise, minFacAux n k = minFacAux n (k+2) using well-founded recursion. If n is odd and 1 < n, then minFacAux n 3 is the smallest prime factor of n.

      Equations
      Instances For
        def Nat.minFac (n : ) :

        Returns the smallest prime factor of n ≠ 1.

        Equations
        Instances For
          @[simp]
          @[simp]
          theorem Nat.minFac_eq (n : ) :
          Nat.minFac n = if 2 n then 2 else Nat.minFacAux n 3
          theorem Nat.minFacAux_has_prop {n : } (n2 : 2 n) (k : ) (i : ) :
          k = 2 * i + 3(∀ (m : ), 2 mm nk m)Nat.minFacProp n (Nat.minFacAux n k)
          theorem Nat.minFac_prime {n : } (n1 : n 1) :
          theorem Nat.minFac_le_of_dvd {n : } {m : } :
          2 mm nNat.minFac n m
          theorem Nat.minFac_le {n : } (H : 0 < n) :
          theorem Nat.le_minFac {m : } {n : } :
          n = 1 m Nat.minFac n ∀ (p : ), Nat.Prime pp nm p
          theorem Nat.le_minFac' {m : } {n : } :
          n = 1 m Nat.minFac n ∀ (p : ), 2 pp nm p
          @[simp]
          theorem Nat.Prime.minFac_eq {p : } (hp : Nat.Prime p) :

          This instance is faster in the virtual machine than decidablePrime1, but slower in the kernel.

          If you need to prove that a particular number is prime, in any case you should not use by decide, but rather by norm_num, which is much faster.

          Equations
          theorem Nat.minFac_le_div {n : } (pos : 0 < n) (np : ¬Nat.Prime n) :
          theorem Nat.minFac_sq_le_self {n : } (w : 0 < n) (h : ¬Nat.Prime n) :

          The square of the smallest prime factor of a composite number n is at most n.

          @[simp]
          theorem Nat.minFac_eq_one_iff {n : } :
          Nat.minFac n = 1 n = 1
          @[simp]
          theorem Nat.minFac_eq_two_iff (n : ) :
          theorem Nat.exists_dvd_of_not_prime {n : } (n2 : 2 n) (np : ¬Nat.Prime n) :
          ∃ (m : ), m n m 1 m n
          theorem Nat.exists_dvd_of_not_prime2 {n : } (n2 : 2 n) (np : ¬Nat.Prime n) :
          ∃ (m : ), m n 2 m m < n
          theorem Nat.exists_prime_and_dvd {n : } (hn : n 1) :
          ∃ (p : ), Nat.Prime p p n
          theorem Nat.dvd_of_forall_prime_mul_dvd {a : } {b : } (hdvd : ∀ (p : ), Nat.Prime pp ap * a b) :
          a b
          theorem Nat.exists_infinite_primes (n : ) :
          ∃ (p : ), n p Nat.Prime p

          Euclid's theorem on the infinitude of primes. Here given in the form: for every n, there exists a prime number p ≥ n.

          theorem Nat.Prime.eq_two_or_odd {p : } (hp : Nat.Prime p) :
          p = 2 p % 2 = 1
          theorem Nat.Prime.eq_two_or_odd' {p : } (hp : Nat.Prime p) :
          p = 2 Odd p
          theorem Nat.Prime.even_iff {p : } (hp : Nat.Prime p) :
          Even p p = 2
          theorem Nat.Prime.odd_of_ne_two {p : } (hp : Nat.Prime p) (h_two : p 2) :
          Odd p
          theorem Nat.Prime.even_sub_one {p : } (hp : Nat.Prime p) (h2 : p 2) :
          Even (p - 1)

          A prime p satisfies p % 2 = 1 if and only if p ≠ 2.

          theorem Nat.coprime_of_dvd {m : } {n : } (H : ∀ (k : ), Nat.Prime kk m¬k n) :
          theorem Nat.coprime_of_dvd' {m : } {n : } (H : ∀ (k : ), Nat.Prime kk mk nk 1) :
          theorem Nat.factors_lemma {k : } :
          (k + 2) / Nat.minFac (k + 2) < k + 2
          theorem Nat.Prime.not_coprime_iff_dvd {m : } {n : } :
          ¬Nat.Coprime m n ∃ (p : ), Nat.Prime p p m p n
          theorem Nat.Prime.dvd_mul {p : } {m : } {n : } (pp : Nat.Prime p) :
          p m * n p m p n
          theorem Nat.Prime.not_dvd_mul {p : } {m : } {n : } (pp : Nat.Prime p) (Hm : ¬p m) (Hn : ¬p n) :
          ¬p m * n
          @[simp]
          @[simp]
          theorem Nat.Coprime.odd_of_left {n : } :
          Nat.Coprime 2 nOdd n

          Alias of the forward direction of Nat.coprime_two_left.

          theorem Odd.coprime_two_left {n : } :
          Odd nNat.Coprime 2 n

          Alias of the reverse direction of Nat.coprime_two_left.

          theorem Nat.Coprime.odd_of_right {n : } :
          Nat.Coprime n 2Odd n

          Alias of the forward direction of Nat.coprime_two_right.

          theorem Odd.coprime_two_right {n : } :
          Odd nNat.Coprime n 2

          Alias of the reverse direction of Nat.coprime_two_right.

          theorem Prime.nat_prime {p : } :

          Alias of the reverse direction of Nat.prime_iff.

          theorem Nat.Prime.prime {p : } :

          Alias of the forward direction of Nat.prime_iff.

          theorem Nat.Prime.dvd_of_dvd_pow {p : } {m : } {n : } (pp : Nat.Prime p) (h : p m ^ n) :
          p m
          theorem Nat.Prime.not_prime_pow' {x : } {n : } (hn : n 1) :
          theorem Nat.Prime.not_prime_pow {x : } {n : } (hn : 2 n) :
          theorem Nat.Prime.eq_one_of_pow {x : } {n : } (h : Nat.Prime (x ^ n)) :
          n = 1
          theorem Nat.Prime.pow_eq_iff {p : } {a : } {k : } (hp : Nat.Prime p) :
          a ^ k = p a = p k = 1
          theorem Nat.pow_minFac {n : } {k : } (hk : k 0) :
          theorem Nat.Prime.pow_minFac {p : } {k : } (hp : Nat.Prime p) (hk : k 0) :
          Nat.minFac (p ^ k) = p
          theorem Nat.Prime.mul_eq_prime_sq_iff {x : } {y : } {p : } (hp : Nat.Prime p) (hx : x 1) (hy : y 1) :
          x * y = p ^ 2 x = p y = p
          theorem Nat.Prime.dvd_factorial {n : } {p : } :
          theorem Nat.Prime.coprime_pow_of_not_dvd {p : } {m : } {a : } (pp : Nat.Prime p) (h : ¬p a) :
          Nat.Coprime a (p ^ m)
          theorem Nat.coprime_primes {p : } {q : } (pp : Nat.Prime p) (pq : Nat.Prime q) :
          theorem Nat.coprime_pow_primes {p : } {q : } (n : ) (m : ) (pp : Nat.Prime p) (pq : Nat.Prime q) (h : p q) :
          Nat.Coprime (p ^ n) (q ^ m)
          theorem Nat.coprime_or_dvd_of_prime {p : } (pp : Nat.Prime p) (i : ) :
          theorem Nat.coprime_of_lt_prime {n : } {p : } (n_pos : 0 < n) (hlt : n < p) (pp : Nat.Prime p) :
          theorem Nat.eq_or_coprime_of_le_prime {n : } {p : } (n_pos : 0 < n) (hle : n p) (pp : Nat.Prime p) :
          p = n Nat.Coprime p n
          theorem Nat.dvd_prime_pow {p : } (pp : Nat.Prime p) {m : } {i : } :
          i p ^ m ∃ k ≤ m, i = p ^ k
          theorem Nat.Prime.dvd_mul_of_dvd_ne {p1 : } {p2 : } {n : } (h_neq : p1 p2) (pp1 : Nat.Prime p1) (pp2 : Nat.Prime p2) (h1 : p1 n) (h2 : p2 n) :
          p1 * p2 n
          theorem Nat.eq_prime_pow_of_dvd_least_prime_pow {a : } {p : } {k : } (pp : Nat.Prime p) (h₁ : ¬a p ^ k) (h₂ : a p ^ (k + 1)) :
          a = p ^ (k + 1)

          If p is prime, and a doesn't divide p^k, but a does divide p^(k+1) then a = p^(k+1).

          theorem Nat.ne_one_iff_exists_prime_dvd {n : } :
          n 1 ∃ (p : ), Nat.Prime p p n
          theorem Nat.eq_one_iff_not_exists_prime_dvd {n : } :
          n = 1 ∀ (p : ), Nat.Prime p¬p n
          theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : } (p_prime : Nat.Prime p) {m : } {n : } {k : } {l : } (hpm : p ^ k m) (hpn : p ^ l n) (hpmn : p ^ (k + l + 1) m * n) :
          p ^ (k + 1) m p ^ (l + 1) n
          theorem Nat.Prime.pow_inj {p : } {q : } {m : } {n : } (hp : Nat.Prime p) (hq : Nat.Prime q) (h : p ^ (m + 1) = q ^ (n + 1)) :
          p = q m = n

          Two prime powers with positive exponents are equal only when the primes and the exponents are equal.

          The type of prime numbers

          Equations
          Instances For
            Equations
            Equations
            Equations
            theorem Nat.Primes.coe_nat_inj (p : Nat.Primes) (q : Nat.Primes) :
            p = q p = q
            instance Nat.monoid.primePow {α : Type u_1} [Monoid α] :
            Equations
            • Nat.monoid.primePow = { pow := fun (x : α) (p : Nat.Primes) => x ^ p }