theorem Hex.Nat.prime_iff {n : ℕ} : Prime n ↔ _root_.Nat.Prime n

The whole correspondence: the Mathlib-free predicate and Nat.Prime agree. Everything else transports along it.

theorem Hex.Nat.natPrime_of_checkPrime {c : PrimeCert} (h : checkPrime c = true) : _root_.Nat.Prime c.subject

Checker soundness, in Mathlib's vocabulary.

theorem Hex.Nat.natPrime_of_checkPrimeAt {n : ℕ} {c : PrimeCert} (h : (c.subject == n && checkPrime c) = true) : _root_.Nat.Prime n

The single-Bool-slot wrapper, in Mathlib's vocabulary; what the Nat.Prime tactic handler emits.

theorem Hex.Nat.isPrime_iff_natPrime {n : ℕ} : isPrime n = true ↔ _root_.Nat.Prime n

The total decision is exact for Nat.Prime.

theorem Hex.Nat.millerRabin_refutes_natPrime {n a : ℕ} (h : millerRabin n a = false) : ¬_root_.Nat.Prime n

A Miller-Rabin witness refutes Nat.Prime.

theorem Hex.Nat.nextPrime?_natPrime {n : ℕ} {r : Rand} {fuel p : ℕ} {r' : Rand} (h : nextPrime? n r fuel = Except.ok (p, r')) : n < p ∧ _root_.Nat.Prime p ∧ ∀ (q : ℕ), n < q → q < p → ¬_root_.Nat.Prime q

A successful next-prime search, in Mathlib's vocabulary.