Documentation

CompPoly.Fields.BN254.Basic

The BN254 scalar prime field #

r of the BN254 (alt_bn128) curve, 254-bit, 2-adicity 28 (EIP-196).

source
@[reducible]
def BN254.scalarFieldSize :
ℕ
Instances For
    source
    @[reducible, inline]
    abbrev BN254.ScalarField :
    Type
    Instances For
      source
      theorem BN254.ScalarField_is_prime :
      Nat.Prime scalarFieldSize
      source
      instance BN254.instFactPrimeScalarFieldSize :
      Fact (Nat.Prime scalarFieldSize)
      source
      @[instance_reducible]
      instance BN254.instFieldScalarField :
      Field ScalarField