• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
        • Lispfloat
        • Arithmetic-1
        • Number-theory
          • Tonelli-shanks-modular-sqrt-algorithm
          • Defprime
          • Dm::primep
          • Defprime-alias
          • Prime
          • Has-square-root?
          • Prime-fix
          • Secp256k1-group-prime
          • Secp256k1-field-prime
          • Jubjub-subgroup-prime
          • Edwards-bls12-subgroup-prime
          • Bn-254-group-prime
          • Bls12-381-scalar-field-prime
          • Baby-jubjub-subgroup-prime
          • Goldilocks-prime
        • Proof-by-arith
        • Arith-equivs
        • Include-an-arithmetic-book
        • Number-theory
        • Arithmetic-3
        • Arithmetic-2
        • Arithmetic-light
        • Arithmetic-5
      • Bit-vectors
      • Algebra
    • Testing-utilities
  • Arithmetic
  • Kestrel-books

Number-theory

Some utilities related to number theory

Subtopics

Tonelli-shanks-modular-sqrt-algorithm
Tonelli-Shanks Modular Square Root Algorithm.
Defprime
Introduce a prime and related machinery.
Dm::primep
Recognizer of prime numbers.
Defprime-alias
Introduce an alias of an existing prime introduced with defprime.
Prime
Fixtype of prime numbers.
Has-square-root?
Modular square root
Prime-fix
Fixer for dm::primep.
Secp256k1-group-prime
A prime defined by defprime.
Secp256k1-field-prime
A prime defined by defprime.
Jubjub-subgroup-prime
A prime defined by defprime.
Edwards-bls12-subgroup-prime
A prime defined by defprime.
Bn-254-group-prime
A prime defined by defprime.
Bls12-381-scalar-field-prime
A prime defined by defprime.
Baby-jubjub-subgroup-prime
A prime defined by defprime.
Goldilocks-prime
A prime defined by defprime.