theorem Hex.PrimalityTactic.isNat_prime {n n' : ℕ} : Mathlib.Meta.NormNum.IsNat n n' → _root_.Nat.Prime n' → _root_.Nat.Prime n

def Hex.PrimalityTactic.evalNatPrimeCert : Mathlib.Meta.NormNum.NormNumExt

The opt-in norm_num extension for certificate-backed Nat.Prime verdicts at and above natPrimeCertThreshold.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PrimalityTactic.evalPrimalityTacNat : Lean.Elab.Tactic.Tactic

The Nat.Prime goal handler for bare primality: same search, same reified certificate, emitted through the Nat.Prime-flavoured wrapper.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PrimalityTactic.evalNatPrimeTrial : Mathlib.Meta.NormNum.NormNumExt

A threshold-guarded alias of Mathlib's trial-division extension. It keeps small numerals working under use_hex_primality_norm_num but declines at the certificate tier, so exhaustion there cannot start a large trial search.

Equations

• One or more equations did not get rendered due to their size.

def useHexPrimalityNormNum : Lean.ParserDescr

Opt the current module into Hex's thresholded Nat.Prime norm_num policy. The choice must be repeated by importers.

Equations

• useHexPrimalityNormNum = Lean.ParserDescr.node `useHexPrimalityNormNum 1024 (Lean.ParserDescr.symbol "use_hex_primality_norm_num")