Documentation

CompPoly.Fields.BN254

The BN254 scalar prime field #

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