Documentation

The characteristic of a finite field on the type level. The characteristic is: For any element x in the field f with characteristic c, we have: c * x = x + x + .. + x (c times) = 0

Characteristic of a field. It takes a finite field type in the proxy value and gives the characteristic. This is done using type families To support new finite field types, you need to add a type instance for the type family Characteristic.

Type family which gives the degree of a polynomial type. This is used to extract type level information from Extension

Type family which gives the size of a field, i.e. the number of elements of a finite field.