# mathlib3documentation

data.nat.prime_norm_num

# Primality prover #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides a norm_num extention to prove that natural numbers are prime.

theorem tactic.norm_num.is_prime_helper (n : ) (h₁ : 1 < n) (h₂ : n.min_fac = n) :
def tactic.norm_num.min_fac_helper (n k : ) :
Prop

A predicate representing partial progress in a proof of min_fac.

Equations
theorem tactic.norm_num.min_fac_helper.n_pos {n k : } (h : k) :
0 < n
theorem tactic.norm_num.min_fac_helper_0 (n : ) (h : 0 < n) :
theorem tactic.norm_num.min_fac_helper_1 {n k k' : } (e : k + 1 = k') (np : (bit1 n).min_fac bit1 k) (h : k) :
theorem tactic.norm_num.min_fac_helper_2 (n k k' : ) (e : k + 1 = k') (np : ¬nat.prime (bit1 k)) (h : k) :
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 : k) :
theorem tactic.norm_num.min_fac_helper_4 (n k : ) (hd : bit1 n % bit1 k = 0) (h : k) :
theorem tactic.norm_num.min_fac_helper_5 (n k k' : ) (e : bit1 k * bit1 k = k') (hd : bit1 n < k') (h : k) :
meta def tactic.norm_num.prove_non_prime (e : expr) (n d₁ : ) :

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

meta def tactic.norm_num.prove_min_fac_aux (a a1 : expr) (n1 : ) :

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

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

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
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 : l) :
(b :: l)
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 : l) :
(b :: l)
theorem tactic.norm_num.factors_helper_sn (n a : ) (h₁ : a < n) (h₂ : n.min_fac = n) :
theorem tactic.norm_num.factors_helper_same (n m a : ) (l : list ) (h : a * m = n) (H : l) :
(a :: l)
theorem tactic.norm_num.factors_helper_end (n : ) (l : list ) (H : l) :

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

Evaluates the prime and min_fac functions.