A library about prime fields.

The prime-fields library contains executable formal specifications of
prime fields and related operations, along with a number of rules about
those operations. The elements of the field corresponding to the
prime `p` are the natural numbers less
than `p`.

To define the notion of primality, we currently use the
function `rtl::primep` defined
in `[books]/projects/quadratic-reciprocity/euclid`.

The following `include-book` command may be helpful to bring in the library:

(include-book "kestrel/prime-fields/prime-fields" :dir :system)

The key functions in the library are:

`(fep x p)`: The "Field-element predicate". Tests whetherx is an element of the field for the primep .`(add x y p)`: Addition in the field: Computes the sum ofx andy modulo the primep .`(sub x y p)`: Subtraction in the field: Computes the difference ofx andy modulo the primep .`(neg x p)`: Negation (additive inverse) in the field: Computes the (unary) negation ofx modulo the primep .`(mul x y p)`: Multiplication in the field: Computes the product ofx andy modulo the primep .`(pow x n p)`: Exponentiation in the field: Computesx to the nth power (x^n ) modulo the primep . Note thatn can be any natural.`(inv x p)`: Multiplicative inverse in the field: Computes1/x modulo the primep . Requiresx to be non-zero.`(div x y p)`: Division in the field: Computesx/y modulo the primep . Requiresy to be non-zero.`(minus1 p)`: Returnsp-1 . Ifp is large, this value will be large as well, but it can help to think of it as-1 .