• 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

• Number-theory

Baby-jubjub-subgroup-prime

A prime defined by defprime.

The value of baby-jubjub-subgroup-prime is 2736030358979909402780800718157159386076813972158567259200215660948447373041.