# Documentation

Mathlib.Tactic.NormNum.Prime

# norm_num extensions on natural numbers #

This file provides a norm_num extension to prove that natural numbers are prime and compute its minimal factor. Todo: compute the list of all factors.

## Implementation Notes #

For numbers larger than 25 bits, the primality proof produced by norm_num is an expression that is thousands of levels deep, and the Lean kernel seems to raise a stack overflow when type-checking that proof. If we want an implementation that works for larger primes, we should generate a proof that has a smaller depth.

Note: evalMinFac.aux does not raise a stack overflow, which can be checked by replacing the prf' in the recursive call by something like (.sort .zero)

theorem Mathlib.Meta.NormNum.not_prime_mul_of_ble (a : ) (b : ) (n : ) (h : a * b = n) (h₁ : Nat.ble a 1 = false) (h₂ : Nat.ble b 1 = false) :

A predicate representing partial progress in a proof of minFac.

Instances For
theorem Mathlib.Meta.NormNum.minFacHelper_0 (n : ) (h1 : Nat.ble 2 n = true) (h2 : 1 = n % 2) :
theorem Mathlib.Meta.NormNum.minFacHelper_1 {n : } {k : } {k' : } (e : k + 2 = k') (h : ) (np : k) :
theorem Mathlib.Meta.NormNum.minFacHelper_2 {n : } {k : } {k' : } (e : k + 2 = k') (nk : ) (h : ) :
theorem Mathlib.Meta.NormNum.minFacHelper_3 {n : } {k : } {k' : } (e : k + 2 = k') (nk : Nat.beq (n % k) 0 = false) (h : ) :
theorem Mathlib.Meta.NormNum.isNat_minFac_2 {a : } {a' : } :
a' % 2 = 0
theorem Mathlib.Meta.NormNum.isNat_minFac_3 {n : } {n' : } (k : ) :
0 = n' % k
theorem Mathlib.Meta.NormNum.isNat_minFac_4 {n : } {n' : } {k : } :
Nat.ble (k * k) n' = false

The norm_num extension which identifies expressions of the form minFac n.

Instances For
theorem Mathlib.Meta.NormNum.isNat_prime_2 {n : } {n' : } :
Nat.ble 2 n' = true
theorem Mathlib.Meta.NormNum.isNat_not_prime {n : } {n' : } (h : ) :
¬

The norm_num extension which identifies expressions of the form Nat.Prime n.

Instances For