Finite fields #
This file contains basic results about finite fields.
Throughout most of this file, K
denotes a finite field
and q
is notation for the cardinality of K
.
See ring_theory.integral_domain
for the fact that the unit group of a finite field is a
cyclic group, as well as the fact that every finite integral domain is a field
(fintype.field_of_domain
).
Main results #
fintype.card_units
: The unit group of a finite field is has cardinalityq - 1
.sum_pow_units
: The sum ofx^i
, wherex
ranges over the units ofK
, isq-1
ifq-1 ∣ i
0
otherwise
finite_field.card
: The cardinalityq
is a power of the characteristic ofK
. Seecard'
for a variant.
Notation #
Throughout most of this file, K
denotes a finite field
and q
is notation for the cardinality of K
.
Implementation notes #
While fintype Kˣ
can be inferred from fintype K
in the presence of decidable_eq K
,
in this file we take the fintype Kˣ
argument directly to reduce the chance of typeclass
diamonds, as fintype
carries data.
The cardinality of a field is at most n
times the cardinality of the image of a degree n
polynomial
If f
and g
are quadratic polynomials, then the f.eval a + g.eval b = 0
has a solution.
The sum of x ^ i
as x
ranges over the units of a finite field of cardinality q
is equal to 0
unless (q - 1) ∣ i
, in which case the sum is q - 1
.
The sum of x ^ i
as x
ranges over a finite field of cardinality q
is equal to 0
if i < q - 1
.
The Fermat-Euler totient theorem. nat.modeq.pow_totient
is an alternative statement
of the same theorem.
The Fermat-Euler totient theorem. zmod.pow_totient
is an alternative statement
of the same theorem.
A variation on Fermat's little theorem. See zmod.pow_card_sub_one_eq_one
The finite field F
has even cardinality iff it has characteristic 2
.