Documentation

CompPoly.Fields.BN254

The BN254 scalar prime field #

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
      @[implicit_reducible]
      instance BN254.instFieldScalarField :
      Field ScalarField