Documentation

Mathlib.Tactic.Primality.Producers

Producers #

This file builds primality certificates from the witnesses the user provides.

source
inductive Mathlib.Tactic.Primality.Witness :
Type

The witness of a primality certificate for one prime, tagged by the certificate type.

Instances For
    source
    inductive Mathlib.Tactic.Primality.CertMode :
    Type

    The witnesses of a certificate.

    • witnesses (witnesses : List Witness) : CertMode

      The certificate with a list of explicit witnesses in witnesses. A prime p takes the first entry whose factors are the prime factors of p - 1 and whose root is a primitive root of p.

    Instances For
      source
      def Mathlib.Tactic.Primality.witnessFor (witnesses : List Witness) (p : ℕ) :
      Lean.CoreM (ℕ × List (ℕ × ℕ))

      Find the root and the factorization of p - 1 given by the first entry of witnesses that is a Lucas witness for the prime p.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Mathlib.Tactic.Primality.normNumBound :
        ℕ

        Numbers below this bound are proved prime by norm_num's evaluation of Nat.minFac.

        Equations
        Instances For
          source
          def Mathlib.Tactic.Primality.Cert.ofWitnesses (witnesses : List Witness) (known : Std.HashSet ℕ) (p : ℕ) :
          Lean.CoreM Cert

          Builds the certificate of p from the first entry of witnesses that fits each prime, with norm_num below normNumBound and the user's proofs for the primes in known. Each prime's certificate is built once.

          Equations
          Instances For