mathlib documentation

data.nat.prime_norm_num

Primality prover #

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_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) :
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) :
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.

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

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

Evaluates the prime and min_fac functions.