mathlib documentation

data.nat.prime

Prime numbers #

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

Important declarations #

source
def nat.prime (p : ℕ) :
Prop

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
source
theorem irreducible_iff_nat_prime (a : ℕ) :
irreducible a ↔ nat.prime a
source
theorem nat.not_prime_zero  :
¬nat.prime 0
source
theorem nat.not_prime_one  :
¬nat.prime 1
source
theorem nat.prime.ne_zero {n : ℕ} (h : nat.prime n) :
n ≠ 0
source
theorem nat.prime.pos {p : ℕ} (pp : nat.prime p) :
0 < p
source
theorem nat.prime.two_le {p : ℕ} :
nat.prime p → 2 ≤ p
source
theorem nat.prime.one_lt {p : ℕ} :
nat.prime p → 1 < p
source
@[protected, instance]
def nat.prime.one_lt' (p : ℕ) [hp : fact (nat.prime p)] :
fact (1 < p)
source
theorem nat.prime.ne_one {p : ℕ} (hp : nat.prime p) :
p ≠ 1
source
theorem nat.two_le_iff (n : ℕ) :
2 ≤ n ↔ n ≠ 0 ∧ ¬is_unit n
source
theorem nat.prime.eq_one_or_self_of_dvd {p : ℕ} (pp : nat.prime p) (m : ℕ) (hm : m ∣ p) :
m = 1 ∨ m = p
source
theorem nat.prime_def_lt'' {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
source
theorem nat.prime_def_lt {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1
source
theorem nat.prime_def_lt' {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p
source
theorem nat.prime_def_le_sqrt {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ nat.sqrt p → ¬m ∣ p
source
theorem nat.prime_of_coprime (n : ℕ) (h1 : 1 < n) (h : ∀ (m : ℕ), m < n → m ≠ 0 → n.coprime m) :
nat.prime n
source
def nat.decidable_prime_1 (p : ℕ) :
decidable (nat.prime p)

This instance is slower than the instance decidable_prime 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 dec_trivial, but rather by norm_num, which is much faster.

Equations
source
theorem nat.prime_two  :
nat.prime 2
source
theorem nat.prime.pred_pos {p : ℕ} (pp : nat.prime p) :
0 < p.pred
source
theorem nat.succ_pred_prime {p : ℕ} (pp : nat.prime p) :
p.pred.succ = p
source
theorem nat.dvd_prime {p m : ℕ} (pp : nat.prime p) :
m ∣ p ↔ m = 1 ∨ m = p
source
theorem nat.dvd_prime_two_le {p m : ℕ} (pp : nat.prime p) (H : 2 ≤ m) :
m ∣ p ↔ m = p
source
theorem nat.prime_dvd_prime_iff_eq {p q : ℕ} (pp : nat.prime p) (qp : nat.prime q) :
p ∣ q ↔ p = q
source
theorem nat.prime.not_dvd_one {p : ℕ} (pp : nat.prime p) :
¬p ∣ 1
source
theorem nat.not_prime_mul {a b : ℕ} (a1 : 1 < a) (b1 : 1 < b) :
¬nat.prime (a * b)
source
theorem nat.not_prime_mul' {a b n : ℕ} (h : a * b = n) (h₁ : 1 < a) (h₂ : 1 < b) :
¬nat.prime n
source
theorem nat.prime_mul_iff {a b : ℕ} :
nat.prime (a * b) ↔ nat.prime a ∧ b = 1 ∨ nat.prime b ∧ a = 1
source
theorem nat.prime.dvd_iff_eq {p a : ℕ} (hp : nat.prime p) (a1 : a ≠ 1) :
a ∣ p ↔ p = a
source
theorem nat.min_fac_lemma (n k : ℕ) (h : ¬n < k * k) :
nat.sqrt n - k < nat.sqrt n + 2 - k
source
def nat.min_fac_aux (n : ℕ) :
ℕ → ℕ

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

Equations
source
def nat.min_fac  :
ℕ → ℕ

Returns the smallest prime factor of n ≠ 1.

Equations
source
@[simp]
theorem nat.min_fac_zero  :
0.min_fac = 2
source
@[simp]
theorem nat.min_fac_one  :
1.min_fac = 1
source
theorem nat.min_fac_eq (n : ℕ) :
n.min_fac = ite (2 ∣ n) 2 (n.min_fac_aux 3)
source
theorem nat.min_fac_aux_has_prop {n : ℕ} (n2 : 2 ≤ n) (k i : ℕ) :
k = 2 * i + 3 → (∀ (m : ℕ), 2 ≤ m → m ∣ n → k ≤ m) → min_fac_prop n (n.min_fac_aux k)
source
theorem nat.min_fac_has_prop {n : ℕ} (n1 : n ≠ 1) :
min_fac_prop n n.min_fac
source
theorem nat.min_fac_dvd (n : ℕ) :
n.min_fac ∣ n
source
theorem nat.min_fac_prime {n : ℕ} (n1 : n ≠ 1) :
nat.prime n.min_fac
source
theorem nat.min_fac_le_of_dvd {n m : ℕ} :
2 ≤ m → m ∣ n → n.min_fac ≤ m
source
theorem nat.min_fac_pos (n : ℕ) :
0 < n.min_fac
source
theorem nat.min_fac_le {n : ℕ} (H : 0 < n) :
n.min_fac ≤ n
source
theorem nat.le_min_fac {m n : ℕ} :
n = 1 ∨ m ≤ n.min_fac ↔ ∀ (p : ℕ), nat.prime p → p ∣ n → m ≤ p
source
theorem nat.le_min_fac' {m n : ℕ} :
n = 1 ∨ m ≤ n.min_fac ↔ ∀ (p : ℕ), 2 ≤ p → p ∣ n → m ≤ p
source
theorem nat.prime_def_min_fac {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ p.min_fac = p
source
@[simp]
theorem nat.prime.min_fac_eq {p : ℕ} (hp : nat.prime p) :
p.min_fac = p
source
@[protected, instance]
def nat.decidable_prime (p : ℕ) :
decidable (nat.prime p)

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

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

Equations
source
theorem nat.not_prime_iff_min_fac_lt {n : ℕ} (n2 : 2 ≤ n) :
¬nat.prime n ↔ n.min_fac < n
source
theorem nat.min_fac_le_div {n : ℕ} (pos : 0 < n) (np : ¬nat.prime n) :
n.min_fac ≤ n / n.min_fac
source
theorem nat.min_fac_sq_le_self {n : ℕ} (w : 0 < n) (h : ¬nat.prime n) :
n.min_fac ^ 2 ≤ n

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

source
@[simp]
theorem nat.min_fac_eq_one_iff {n : ℕ} :
n.min_fac = 1 ↔ n = 1
source
@[simp]
theorem nat.min_fac_eq_two_iff (n : ℕ) :
n.min_fac = 2 ↔ 2 ∣ n
source
theorem nat.exists_dvd_of_not_prime {n : ℕ} (n2 : 2 ≤ n) (np : ¬nat.prime n) :
∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n
source
theorem nat.exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬nat.prime n) :
∃ (m : ℕ), m ∣ n ∧ 2 ≤ m ∧ m < n
source
theorem nat.exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) :
∃ (p : ℕ), nat.prime p ∧ p ∣ n
source
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.

source
theorem nat.not_bdd_above_set_of_prime  :
¬bdd_above {p : ℕ | nat.prime p}

A version of nat.exists_infinite_primes using the bdd_above predicate.

source
theorem nat.infinite_set_of_prime  :
{p : ℕ | nat.prime p}.infinite

A version of nat.exists_infinite_primes using the set.infinite predicate.

source
theorem nat.prime.eq_two_or_odd {p : ℕ} (hp : nat.prime p) :
p = 2 ∨ p % 2 = 1
source
theorem nat.prime.eq_two_or_odd' {p : ℕ} (hp : nat.prime p) :
p = 2 ∨ odd p
source
theorem nat.prime.mod_two_eq_one_iff_ne_two {p : ℕ} [fact (nat.prime p)] :
p % 2 = 1 ↔ p ≠ 2

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

source
theorem nat.coprime_of_dvd {m n : ℕ} (H : ∀ (k : ℕ), nat.prime k → k ∣ m → ¬k ∣ n) :
m.coprime n
source
theorem nat.coprime_of_dvd' {m n : ℕ} (H : ∀ (k : ℕ), nat.prime k → k ∣ m → k ∣ n → k ∣ 1) :
m.coprime n
source
theorem nat.factors_lemma {k : ℕ} :
(k + 2) / (k + 2).min_fac < k + 2
source
def nat.factors  :
ℕ → list ℕ

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

Equations
source
@[simp]
theorem nat.factors_zero  :
0.factors = list.nil
source
@[simp]
theorem nat.factors_one  :
1.factors = list.nil
source
theorem nat.prime_of_mem_factors {n p : ℕ} :
p ∈ n.factors → nat.prime p
source
theorem nat.pos_of_mem_factors {n p : ℕ} (h : p ∈ n.factors) :
0 < p
source
theorem nat.prod_factors {n : ℕ} :
n ≠ 0 → n.factors.prod = n
source
theorem nat.factors_prime {p : ℕ} (hp : nat.prime p) :
p.factors = [p]
source
theorem nat.factors_chain {n a : ℕ} :
(∀ (p : ℕ), nat.prime p → p ∣ n → a ≤ p) → list.chain has_le.le a n.factors
source
theorem nat.factors_chain_2 (n : ℕ) :
list.chain has_le.le 2 n.factors
source
theorem nat.factors_chain' (n : ℕ) :
list.chain' has_le.le n.factors
source
theorem nat.factors_sorted (n : ℕ) :
list.sorted has_le.le n.factors
source
theorem nat.factors_add_two (n : ℕ) :
(n + 2).factors = (n + 2).min_fac :: ((n + 2) / (n + 2).min_fac).factors

factors can be constructed inductively by extracting min_fac, for sufficiently large n.

source
@[simp]
theorem nat.factors_eq_nil (n : ℕ) :
n.factors = list.nil ↔ n = 0 ∨ n = 1
source
theorem nat.eq_of_perm_factors {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : a.factors ~ b.factors) :
a = b
source
theorem nat.prime.coprime_iff_not_dvd {p n : ℕ} (pp : nat.prime p) :
p.coprime n ↔ ¬p ∣ n
source
theorem nat.prime.dvd_iff_not_coprime {p n : ℕ} (pp : nat.prime p) :
p ∣ n ↔ ¬p.coprime n
source
theorem nat.prime.not_coprime_iff_dvd {m n : ℕ} :
¬m.coprime n ↔ ∃ (p : ℕ), nat.prime p ∧ p ∣ m ∧ p ∣ n
source
theorem nat.prime.dvd_mul {p m n : ℕ} (pp : nat.prime p) :
p ∣ m * n ↔ p ∣ m ∨ p ∣ n
source
theorem nat.prime.not_dvd_mul {p m n : ℕ} (pp : nat.prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) :
¬p ∣ m * n
source
theorem nat.prime_iff {p : ℕ} :
nat.prime p ↔ prime p
source
theorem nat.irreducible_iff_prime {p : ℕ} :
irreducible p ↔ prime p
source
theorem nat.prime.dvd_of_dvd_pow {p m n : ℕ} (pp : nat.prime p) (h : p ∣ m ^ n) :
p ∣ m
source
theorem nat.prime.pow_not_prime {x n : ℕ} (hn : 2 ≤ n) :
¬nat.prime (x ^ n)
source
theorem nat.prime.pow_not_prime' {x n : ℕ} :
n ≠ 1 → ¬nat.prime (x ^ n)
source
theorem nat.prime.eq_one_of_pow {x n : ℕ} (h : nat.prime (x ^ n)) :
n = 1
source
theorem nat.prime.pow_eq_iff {p a k : ℕ} (hp : nat.prime p) :
a ^ k = p ↔ a = p ∧ k = 1
source
theorem nat.pow_min_fac {n k : ℕ} (hk : k ≠ 0) :
(n ^ k).min_fac = n.min_fac
source
theorem nat.prime.pow_min_fac {p k : ℕ} (hp : nat.prime p) (hk : k ≠ 0) :
(p ^ k).min_fac = p
source
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
source
theorem nat.prime.dvd_factorial {n p : ℕ} (hp : nat.prime p) :
p ∣ n! ↔ p ≤ n
source
theorem nat.prime.coprime_pow_of_not_dvd {p m a : ℕ} (pp : nat.prime p) (h : ¬p ∣ a) :
a.coprime (p ^ m)
source
theorem nat.coprime_primes {p q : ℕ} (pp : nat.prime p) (pq : nat.prime q) :
p.coprime q ↔ p ≠ q
source
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)
source
theorem nat.coprime_or_dvd_of_prime {p : ℕ} (pp : nat.prime p) (i : ℕ) :
p.coprime i ∨ p ∣ i
source
theorem nat.coprime_of_lt_prime {n p : ℕ} (n_pos : 0 < n) (hlt : n < p) (pp : nat.prime p) :
p.coprime n
source
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
source
theorem nat.dvd_prime_pow {p : ℕ} (pp : nat.prime p) {m i : ℕ} :
i ∣ p ^ m ↔ ∃ (k : ℕ) (H : k ≤ m), i = p ^ k
source
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
source
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).

source
theorem nat.ne_one_iff_exists_prime_dvd {n : ℕ} :
n ≠ 1 ↔ ∃ (p : ℕ), nat.prime p ∧ p ∣ n
source
theorem nat.eq_one_iff_not_exists_prime_dvd {n : ℕ} :
n = 1 ↔ ∀ (p : ℕ), nat.prime p → ¬p ∣ n
source
theorem nat.mem_factors_iff_dvd {n p : ℕ} (hn : n ≠ 0) (hp : nat.prime p) :
p ∈ n.factors ↔ p ∣ n
source
theorem nat.dvd_of_mem_factors {n p : ℕ} (h : p ∈ n.factors) :
p ∣ n
source
theorem nat.mem_factors {n p : ℕ} (hn : n ≠ 0) :
p ∈ n.factors ↔ nat.prime p ∧ p ∣ n
source
theorem nat.le_of_mem_factors {n p : ℕ} (h : p ∈ n.factors) :
p ≤ n
source
theorem nat.factors_unique {n : ℕ} {l : list ℕ} (h₁ : l.prod = n) (h₂ : ∀ (p : ℕ), p ∈ l → nat.prime p) :
l ~ n.factors

Fundamental theorem of arithmetic

source
theorem nat.prime.factors_pow {p : ℕ} (hp : nat.prime p) (n : ℕ) :
(p ^ n).factors = list.repeat p n
source
theorem nat.eq_prime_pow_of_unique_prime_dvd {n p : ℕ} (hpos : n ≠ 0) (h : ∀ {d : ℕ}, nat.prime d → d ∣ n → d = p) :
n = p ^ n.factors.length
source
theorem nat.perm_factors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a * b).factors ~ a.factors ++ b.factors

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

source
theorem nat.perm_factors_mul_of_coprime {a b : ℕ} (hab : a.coprime b) :
(a * b).factors ~ a.factors ++ b.factors

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

source
theorem nat.factors_sublist_right {n k : ℕ} (h : k ≠ 0) :
n.factors <+ (n * k).factors
source
theorem nat.factors_sublist_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) :
n.factors <+ k.factors
source
theorem nat.factors_subset_right {n k : ℕ} (h : k ≠ 0) :
n.factors ⊆ (n * k).factors
source
theorem nat.factors_subset_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) :
n.factors ⊆ k.factors
source
theorem nat.dvd_of_factors_subperm {a b : ℕ} (ha : a ≠ 0) (h : a.factors <+~ b.factors) :
a ∣ b
source
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
source
theorem nat.prime_iff_prime_int {p : ℕ} :
nat.prime p ↔ prime ↑p
source
def nat.primes  :
Type

The type of prime numbers

Equations
source
@[protected, instance]
def nat.primes.has_repr  :
has_repr nat.primes
Equations
source
@[protected, instance]
def nat.primes.inhabited_primes  :
inhabited nat.primes
Equations
source
@[protected, instance]
def nat.primes.coe_nat  :
has_coe nat.primes ℕ
Equations
source
theorem nat.primes.coe_nat_inj (p q : nat.primes) :
↑p = ↑q → p = q
source
@[protected, instance]
def nat.monoid.prime_pow {α : Type u_1} [monoid α] :
has_pow α nat.primes
Equations

Primality prover #

source
theorem tactic.norm_num.is_prime_helper (n : ℕ) (h₁ : 1 < n) (h₂ : n.min_fac = n) :
nat.prime n
source
theorem tactic.norm_num.min_fac_bit0 (n : ℕ) :
(bit0 n).min_fac = 2
source
def tactic.norm_num.min_fac_helper (n k : ℕ) :
Prop

A predicate representing partial progress in a proof of min_fac.

Equations
source
theorem tactic.norm_num.min_fac_helper.n_pos {n k : ℕ} (h : tactic.norm_num.min_fac_helper n k) :
0 < n
source
theorem tactic.norm_num.min_fac_ne_bit0 {n k : ℕ} :
(bit1 n).min_fac ≠ bit0 k
source
theorem tactic.norm_num.min_fac_helper_0 (n : ℕ) (h : 0 < n) :
tactic.norm_num.min_fac_helper n 1
source
theorem tactic.norm_num.min_fac_helper_1 {n k k' : ℕ} (e : k + 1 = k') (np : (bit1 n).min_fac ≠ bit1 k) (h : tactic.norm_num.min_fac_helper n k) :
tactic.norm_num.min_fac_helper n k'
source
theorem tactic.norm_num.min_fac_helper_2 (n k k' : ℕ) (e : k + 1 = k') (np : ¬nat.prime (bit1 k)) (h : tactic.norm_num.min_fac_helper n k) :
tactic.norm_num.min_fac_helper n k'
source
theorem tactic.norm_num.min_fac_helper_3 (n k k' c : ℕ) (e : k + 1 = k') (nc : bit1 n % bit1 k = c) (c0 : 0 < c) (h : tactic.norm_num.min_fac_helper n k) :
tactic.norm_num.min_fac_helper n k'
source
theorem tactic.norm_num.min_fac_helper_4 (n k : ℕ) (hd : bit1 n % bit1 k = 0) (h : tactic.norm_num.min_fac_helper n k) :
(bit1 n).min_fac = bit1 k
source
theorem tactic.norm_num.min_fac_helper_5 (n k k' : ℕ) (e : (bit1 k) * bit1 k = k') (hd : bit1 n < k') (h : tactic.norm_num.min_fac_helper n k) :
(bit1 n).min_fac = bit1 n
source
meta def tactic.norm_num.prove_non_prime (e : expr) (n d₁ : ℕ) :
tactic expr

Given e a natural numeral and d : nat a factor of it, return ⊢ ¬ prime e.

source
meta def tactic.norm_num.prove_min_fac_aux (a a1 : expr) (n1 : ℕ) :
tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × expr × expr)

Given a,a1 := bit1 a, n1 the value of a1, b and p : min_fac_helper a b, returns (c, ⊢ min_fac a1 = c).

source
meta def tactic.norm_num.prove_min_fac (ic : tactic.instance_cache) (e : expr) :
tactic (tactic.instance_cache × expr × expr)

Given a a natural numeral, returns (b, ⊢ min_fac a = b).

source
def tactic.norm_num.factors_helper (n p : ℕ) (l : list ℕ) :
Prop

A partial proof of factors. Asserts that l is a sorted list of primes, lower bounded by a prime p, which multiplies to n.

Equations
source
theorem tactic.norm_num.factors_helper_nil (a : ℕ) :
tactic.norm_num.factors_helper 1 a list.nil
source
theorem tactic.norm_num.factors_helper_cons' (n m a b : ℕ) (l : list ℕ) (h₁ : b * m = n) (h₂ : a ≤ b) (h₃ : b.min_fac = b) (H : tactic.norm_num.factors_helper m b l) :
tactic.norm_num.factors_helper n a (b :: l)
source
theorem tactic.norm_num.factors_helper_cons (n m a b : ℕ) (l : list ℕ) (h₁ : b * m = n) (h₂ : a < b) (h₃ : b.min_fac = b) (H : tactic.norm_num.factors_helper m b l) :
tactic.norm_num.factors_helper n a (b :: l)
source
theorem tactic.norm_num.factors_helper_sn (n a : ℕ) (h₁ : a < n) (h₂ : n.min_fac = n) :
tactic.norm_num.factors_helper n a [n]
source
theorem tactic.norm_num.factors_helper_same (n m a : ℕ) (l : list ℕ) (h : a * m = n) (H : tactic.norm_num.factors_helper m a l) :
tactic.norm_num.factors_helper n a (a :: l)
source
theorem tactic.norm_num.factors_helper_same_sn (a : ℕ) :
tactic.norm_num.factors_helper a a [a]
source
theorem tactic.norm_num.factors_helper_end (n : ℕ) (l : list ℕ) (H : tactic.norm_num.factors_helper n 2 l) :
n.factors = l
source
meta def tactic.norm_num.prove_factors_aux  :
tactic.instance_cache → expr → expr → ℕ → ℕ → tactic (tactic.instance_cache × expr × expr)

Given n and a natural numerals, returns (l, ⊢ factors_helper n a l).

source
meta def tactic.norm_num.eval_prime  :
expr → tactic (expr × expr)

Evaluates the prime and min_fac functions.

source
theorem nat.prime_three  :
nat.prime 3
source
@[protected, instance]
def nat.fact_prime_two  :
fact (nat.prime 2)
source
@[protected, instance]
def nat.fact_prime_three  :
fact (nat.prime 3)
source
theorem nat.mem_factors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) {p : ℕ} :
p ∈ (a * b).factors ↔ p ∈ a.factors ∨ p ∈ b.factors
source
theorem nat.factors_mul_to_finset {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a * b).factors.to_finset = a.factors.to_finset ∪ b.factors.to_finset

If a, b are positive, the prime divisors of a * b are the union of those of a and b

source
theorem nat.pow_succ_factors_to_finset (n k : ℕ) :
(n ^ (k + 1)).factors.to_finset = n.factors.to_finset
source
theorem nat.pow_factors_to_finset (n : ℕ) {k : ℕ} (hk : k ≠ 0) :
(n ^ k).factors.to_finset = n.factors.to_finset
source
theorem nat.prime_pow_prime_divisor {p k : ℕ} (hk : k ≠ 0) (hp : nat.prime p) :
(p ^ k).factors.to_finset = {p}

The only prime divisor of positive prime power p^k is p itself

source
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

source
theorem nat.mem_factors_mul_of_coprime {a b : ℕ} (hab : a.coprime b) (p : ℕ) :
p ∈ (a * b).factors ↔ p ∈ a.factors ∪ b.factors
source
theorem nat.factors_mul_to_finset_of_coprime {a b : ℕ} (hab : a.coprime b) :
(a * b).factors.to_finset = a.factors.to_finset ∪ b.factors.to_finset
source
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

source
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

source
theorem nat.eq_two_pow_or_exists_odd_prime_and_dvd (n : ℕ) :
(∃ (k : ℕ), n = 2 ^ k) ∨ ∃ (p : ℕ), nat.prime p ∧ p ∣ n ∧ odd p
source
theorem int.prime_two  :
prime 2
source
theorem int.prime_three  :
prime 3
source
theorem card_multiples (n p : ℕ) :
(finset.filter (λ (e : ℕ), p ∣ e + 1) (finset.range n)).card = n / p

Exactly n / p naturals in [1, n] are multiples of p.