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 : n.Prime) :
    n 0
    theorem Nat.Prime.pos {p : } (pp : p.Prime) :
    0 < p
    theorem Nat.Prime.two_le {p : } :
    p.Prime2 p
    theorem Nat.Prime.one_lt {p : } :
    p.Prime1 < p
    theorem Nat.Prime.one_le {p : } (hp : p.Prime) :
    1 p
    instance Nat.Prime.one_lt' (p : ) [hp : Fact p.Prime] :
    Fact (1 < p)
    Equations
    • =
    theorem Nat.Prime.ne_one {p : } (hp : p.Prime) :
    p 1
    theorem Nat.Prime.eq_one_or_self_of_dvd {p : } (pp : p.Prime) (m : ) (hm : m p) :
    m = 1 m = p
    theorem Nat.prime_def_lt'' {p : } :
    p.Prime 2 p ∀ (m : ), m pm = 1 m = p
    theorem Nat.prime_def_lt {p : } :
    p.Prime 2 p m < p, m pm = 1
    theorem Nat.prime_def_lt' {p : } :
    p.Prime 2 p ∀ (m : ), 2 mm < p¬m p
    theorem Nat.prime_def_le_sqrt {p : } :
    p.Prime 2 p ∀ (m : ), 2 mm p.sqrt¬m p
    theorem Nat.prime_of_coprime (n : ) (h1 : 1 < n) (h : m < n, m 0n.Coprime m) :
    n.Prime
    def Nat.decidablePrime1 (p : ) :
    Decidable p.Prime

    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 : p.Prime) (h_two : p 2) (h_three : p 3) :
      5 p
      theorem Nat.Prime.pred_pos {p : } (pp : p.Prime) :
      0 < p.pred
      theorem Nat.succ_pred_prime {p : } (pp : p.Prime) :
      p.pred.succ = p
      theorem Nat.dvd_prime {p : } {m : } (pp : p.Prime) :
      m p m = 1 m = p
      theorem Nat.dvd_prime_two_le {p : } {m : } (pp : p.Prime) (H : 2 m) :
      m p m = p
      theorem Nat.prime_dvd_prime_iff_eq {p : } {q : } (pp : p.Prime) (qp : q.Prime) :
      p q p = q
      theorem Nat.Prime.not_dvd_one {p : } (pp : p.Prime) :
      ¬p 1
      theorem Nat.prime_mul_iff {a : } {b : } :
      (a * b).Prime a.Prime b = 1 b.Prime a = 1
      theorem Nat.not_prime_mul {a : } {b : } (a1 : a 1) (b1 : b 1) :
      ¬(a * b).Prime
      theorem Nat.not_prime_mul' {a : } {b : } {n : } (h : a * b = n) (h₁ : a 1) (h₂ : b 1) :
      ¬n.Prime
      theorem Nat.Prime.dvd_iff_eq {p : } {a : } (hp : p.Prime) (a1 : a 1) :
      a p p = a
      theorem Nat.minFac_lemma (n : ) (k : ) (h : ¬n < k * k) :
      n.sqrt - k < n.sqrt + 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.

      By default this well-founded recursion would be irreducible. This prevents use decide to resolve Nat.prime n for small values of n, so we mark this as @[semireducible].

      In future, we may want to remove this annotation and instead use norm_num instead of decide in these situations.

      Equations
      • n.minFacAux x = if n < x * x then n else if x n then x else n.minFacAux (x + 2)
      Instances For
        def Nat.minFac (n : ) :

        Returns the smallest prime factor of n ≠ 1.

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

          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.not_prime_iff_minFac_lt {n : } (n2 : 2 n) :
          ¬n.Prime n.minFac < n
          theorem Nat.minFac_le_div {n : } (pos : 0 < n) (np : ¬n.Prime) :
          n.minFac n / n.minFac
          theorem Nat.minFac_sq_le_self {n : } (w : 0 < n) (h : ¬n.Prime) :
          n.minFac ^ 2 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 : } :
          n.minFac = 1 n = 1
          @[simp]
          theorem Nat.minFac_eq_two_iff (n : ) :
          n.minFac = 2 2 n
          theorem Nat.exists_dvd_of_not_prime {n : } (n2 : 2 n) (np : ¬n.Prime) :
          ∃ (m : ), m n m 1 m n
          theorem Nat.exists_dvd_of_not_prime2 {n : } (n2 : 2 n) (np : ¬n.Prime) :
          ∃ (m : ), m n 2 m m < n
          theorem Nat.not_prime_of_dvd_of_ne {m : } {n : } (h1 : m n) (h2 : m 1) (h3 : m n) :
          ¬n.Prime
          theorem Nat.not_prime_of_dvd_of_lt {m : } {n : } (h1 : m n) (h2 : 2 m) (h3 : m < n) :
          ¬n.Prime
          theorem Nat.not_prime_iff_exists_dvd_ne {n : } (h : 2 n) :
          ¬n.Prime ∃ (m : ), m n m 1 m n
          theorem Nat.not_prime_iff_exists_dvd_lt {n : } (h : 2 n) :
          ¬n.Prime ∃ (m : ), m n 2 m m < n
          theorem Nat.exists_prime_and_dvd {n : } (hn : n 1) :
          ∃ (p : ), p.Prime p n
          theorem Nat.dvd_of_forall_prime_mul_dvd {a : } {b : } (hdvd : ∀ (p : ), p.Primep ap * a b) :
          a b
          theorem Nat.exists_infinite_primes (n : ) :
          ∃ (p : ), n p p.Prime

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

          A version of Nat.exists_infinite_primes using the BddAbove predicate.

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

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

          theorem Nat.coprime_of_dvd {m : } {n : } (H : ∀ (k : ), k.Primek m¬k n) :
          m.Coprime n
          theorem Nat.coprime_of_dvd' {m : } {n : } (H : ∀ (k : ), k.Primek mk nk 1) :
          m.Coprime n
          theorem Nat.factors_lemma {k : } :
          (k + 2) / (k + 2).minFac < k + 2
          theorem Nat.Prime.coprime_iff_not_dvd {p : } {n : } (pp : p.Prime) :
          p.Coprime n ¬p n
          theorem Nat.Prime.dvd_iff_not_coprime {p : } {n : } (pp : p.Prime) :
          p n ¬p.Coprime n
          theorem Nat.Prime.not_coprime_iff_dvd {m : } {n : } :
          ¬m.Coprime n ∃ (p : ), p.Prime p m p n
          theorem Nat.Prime.dvd_mul {p : } {m : } {n : } (pp : p.Prime) :
          p m * n p m p n
          theorem Nat.Prime.not_dvd_mul {p : } {m : } {n : } (pp : p.Prime) (Hm : ¬p m) (Hn : ¬p n) :
          ¬p m * n
          @[simp]
          @[simp]
          theorem Nat.coprime_two_right {n : } :
          n.Coprime 2 Odd n
          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 Odd.coprime_two_right {n : } :
          Odd nn.Coprime 2

          Alias of the reverse direction of Nat.coprime_two_right.

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

          Alias of the forward direction of Nat.coprime_two_right.

          theorem Nat.prime_iff {p : } :
          p.Prime Prime p
          theorem Nat.Prime.prime {p : } :
          p.PrimePrime p

          Alias of the forward direction of Nat.prime_iff.

          theorem Prime.nat_prime {p : } :
          Prime pp.Prime

          Alias of the reverse direction of Nat.prime_iff.

          theorem Nat.Prime.dvd_of_dvd_pow {p : } {m : } {n : } (pp : p.Prime) (h : p m ^ n) :
          p m
          theorem Nat.Prime.not_prime_pow' {x : } {n : } (hn : n 1) :
          ¬(x ^ n).Prime
          theorem Nat.Prime.not_prime_pow {x : } {n : } (hn : 2 n) :
          ¬(x ^ n).Prime
          theorem Nat.Prime.eq_one_of_pow {x : } {n : } (h : (x ^ n).Prime) :
          n = 1
          theorem Nat.Prime.pow_eq_iff {p : } {a : } {k : } (hp : p.Prime) :
          a ^ k = p a = p k = 1
          theorem Nat.pow_minFac {n : } {k : } (hk : k 0) :
          (n ^ k).minFac = n.minFac
          theorem Nat.Prime.pow_minFac {p : } {k : } (hp : p.Prime) (hk : k 0) :
          (p ^ k).minFac = p
          theorem Nat.Prime.mul_eq_prime_sq_iff {x : } {y : } {p : } (hp : p.Prime) (hx : x 1) (hy : y 1) :
          x * y = p ^ 2 x = p y = p
          theorem Nat.Prime.dvd_factorial {n : } {p : } :
          p.Prime(p n.factorial p n)
          theorem Nat.Prime.coprime_pow_of_not_dvd {p : } {m : } {a : } (pp : p.Prime) (h : ¬p a) :
          a.Coprime (p ^ m)
          theorem Nat.coprime_primes {p : } {q : } (pp : p.Prime) (pq : q.Prime) :
          p.Coprime q p q
          theorem Nat.coprime_pow_primes {p : } {q : } (n : ) (m : ) (pp : p.Prime) (pq : q.Prime) (h : p q) :
          (p ^ n).Coprime (q ^ m)
          theorem Nat.coprime_or_dvd_of_prime {p : } (pp : p.Prime) (i : ) :
          p.Coprime i p i
          theorem Nat.coprime_of_lt_prime {n : } {p : } (n_pos : 0 < n) (hlt : n < p) (pp : p.Prime) :
          p.Coprime n
          theorem Nat.eq_or_coprime_of_le_prime {n : } {p : } (n_pos : 0 < n) (hle : n p) (pp : p.Prime) :
          p = n p.Coprime n
          theorem Nat.dvd_prime_pow {p : } (pp : p.Prime) {m : } {i : } :
          i p ^ m km, i = p ^ k
          theorem Nat.Prime.dvd_mul_of_dvd_ne {p1 : } {p2 : } {n : } (h_neq : p1 p2) (pp1 : p1.Prime) (pp2 : p2.Prime) (h1 : p1 n) (h2 : p2 n) :
          p1 * p2 n
          theorem Nat.eq_prime_pow_of_dvd_least_prime_pow {a : } {p : } {k : } (pp : p.Prime) (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 : ), p.Prime p n
          theorem Nat.eq_one_iff_not_exists_prime_dvd {n : } :
          n = 1 ∀ (p : ), p.Prime¬p n
          theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : } (p_prime : p.Prime) {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_iff_prime_int {p : } :
          p.Prime Prime p
          theorem Nat.Prime.pow_inj {p : } {q : } {m : } {n : } (hp : p.Prime) (hq : q.Prime) (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.

          theorem Nat.exists_pow_lt_factorial (c : ) :
          n0 > 1, nn0, c ^ n < (n - 1).factorial
          theorem Nat.exists_mul_pow_lt_factorial (a : ) (c : ) :
          ∃ (n0 : ), nn0, a * c ^ n < (n - 1).factorial
          theorem Nat.exists_prime_mul_pow_lt_factorial (n : ) (a : ) (c : ) :
          p > n, p.Prime a * c ^ p < (p - 1).factorial

          The type of prime numbers

          Equations
          Instances For
            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 }