Documentation

Mathlib.Data.Nat.Prime.Basic

Notable Theorems #

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) :
0 < p.pred
theorem Nat.succ_pred_prime {p : } (pp : Nat.Prime p) :
p.pred.succ = p
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.not_prime_of_dvd_of_ne {m : } {n : } (h1 : m n) (h2 : m 1) (h3 : m n) :
theorem Nat.not_prime_of_dvd_of_lt {m : } {n : } (h1 : m n) (h2 : 2 m) (h3 : m < n) :
theorem Nat.not_prime_iff_exists_dvd_ne {n : } (h : 2 n) :
¬Nat.Prime n ∃ (m : ), m n m 1 m n
theorem Nat.not_prime_iff_exists_dvd_lt {n : } (h : 2 n) :
¬Nat.Prime n ∃ (m : ), m n 2 m m < 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.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 mk nk 1) :
m.Coprime n
theorem Nat.Prime.dvd_iff_not_coprime {p : } {n : } (pp : Nat.Prime p) :
p n ¬p.Coprime n
theorem Nat.Prime.not_coprime_iff_dvd {m : } {n : } :
¬m.Coprime n ∃ (p : ), Nat.Prime p 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_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 Nat.Coprime.odd_of_right {n : } :
n.Coprime 2Odd n

Alias of the forward direction of Nat.coprime_two_right.

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

Alias of the reverse direction of Nat.coprime_two_right.

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) :
(n ^ k).minFac = n.minFac
theorem Nat.Prime.pow_minFac {p : } {k : } (hp : Nat.Prime p) (hk : k 0) :
(p ^ k).minFac = 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 : } :
Nat.Prime p(p n.factorial p n)
theorem Nat.Prime.coprime_pow_of_not_dvd {p : } {m : } {a : } (pp : Nat.Prime p) (h : ¬p a) :
a.Coprime (p ^ m)
theorem Nat.coprime_primes {p : } {q : } (pp : Nat.Prime p) (pq : Nat.Prime q) :
p.Coprime q p q
theorem Nat.coprime_pow_primes {p : } {q : } (n : ) (m : ) (pp : Nat.Prime p) (pq : Nat.Prime q) (h : p q) :
(p ^ n).Coprime (q ^ m)
theorem Nat.coprime_or_dvd_of_prime {p : } (pp : Nat.Prime p) (i : ) :
p.Coprime i p i
theorem Nat.coprime_of_lt_prime {n : } {p : } (n_pos : 0 < n) (hlt : n < p) (pp : Nat.Prime p) :
p.Coprime n
theorem Nat.eq_or_coprime_of_le_prime {n : } {p : } (n_pos : 0 < n) (hle : n p) (pp : Nat.Prime p) :
p = n p.Coprime n
theorem Nat.dvd_prime_pow {p : } (pp : Nat.Prime p) {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 : 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.

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, Nat.Prime p a * c ^ p < (p - 1).factorial