# mathlib3documentation

field_theory.finite.basic

# Finite fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

1. fintype.card_units: The unit group of a finite field is has cardinality q - 1.
2. sum_pow_units: The sum of x^i, where x ranges over the units of K, is
• q-1 if q-1 ∣ i
• 0 otherwise
3. finite_field.card: The cardinality q is a power of the characteristic of K. See card' 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.

theorem finite_field.card_image_polynomial_eval {R : Type u_2} [comm_ring R] [is_domain R] [decidable_eq R] [fintype R] {p : polynomial R} (hp : 0 < p.degree) :

The cardinality of a field is at most n times the cardinality of the image of a degree n polynomial

theorem finite_field.exists_root_sum_quadratic {R : Type u_2} [comm_ring R] [is_domain R] [fintype R] {f g : polynomial R} (hf2 : f.degree = 2) (hg2 : g.degree = 2) (hR : = 1) :
(a b : R), + = 0

If f and g are quadratic polynomials, then the f.eval a + g.eval b = 0 has a solution.

theorem finite_field.pow_card_sub_one_eq_one {K : Type u_1} [fintype K] (a : K) (ha : a 0) :
a ^ - 1) = 1
theorem finite_field.pow_card {K : Type u_1} [fintype K] (a : K) :
= a
theorem finite_field.pow_card_pow {K : Type u_1} [fintype K] (n : ) (a : K) :
a ^ = a
theorem finite_field.card (K : Type u_1) [field K] [fintype K] (p : ) [ p] :
(n : ℕ+), = p ^ n
theorem finite_field.card' (K : Type u_1) [field K] [fintype K] :
(p : ) (n : ℕ+), = p ^ n
@[simp]
theorem finite_field.cast_card_eq_zero (K : Type u_1) [field K] [fintype K] :
theorem finite_field.forall_pow_eq_one_iff (K : Type u_1) [field K] [fintype K] (i : ) :
( (x : Kˣ), x ^ i = 1) i
theorem finite_field.sum_pow_units (K : Type u_1) [field K] [fintype K] [fintype Kˣ] (i : ) :
finset.univ.sum (λ (x : Kˣ), x ^ i) = ite - 1 i) (-1) 0

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.

theorem finite_field.sum_pow_lt_card_sub_one {K : Type u_1} [field K] [fintype K] (i : ) (h : i < ) :
finset.univ.sum (λ (x : K), x ^ i) = 0

The sum of x ^ i as x ranges over a finite field of cardinality q is equal to 0 if i < q - 1.

theorem finite_field.X_pow_card_sub_X_nat_degree_eq (K' : Type u_3) [field K'] {p : } (hp : 1 < p) :
theorem finite_field.X_pow_card_pow_sub_X_nat_degree_eq (K' : Type u_3) [field K'] {p n : } (hn : n 0) (hp : 1 < p) :
theorem finite_field.X_pow_card_sub_X_ne_zero (K' : Type u_3) [field K'] {p : } (hp : 1 < p) :
theorem finite_field.X_pow_card_pow_sub_X_ne_zero (K' : Type u_3) [field K'] {p n : } (hn : n 0) (hp : 1 < p) :
0
theorem finite_field.frobenius_pow {K : Type u_1} [field K] [fintype K] {p : } [fact (nat.prime p)] [ p] {n : } (hcard : = p ^ n) :
p ^ n = 1
theorem finite_field.expand_card {K : Type u_1} [field K] [fintype K] (f : polynomial K) :
theorem zmod.sq_add_sq (p : ) [hp : fact (nat.prime p)] (x : zmod p) :
(a b : zmod p), a ^ 2 + b ^ 2 = x
theorem char_p.sq_add_sq (R : Type u_1) [comm_ring R] [is_domain R] (p : ) [ne_zero p] [ p] (x : ) :
(a b : ), a ^ 2 + b ^ 2 = x
@[simp]
theorem zmod.pow_totient {n : } (x : (zmod n)ˣ) :
x ^ n.totient = 1

The Fermat-Euler totient theorem. nat.modeq.pow_totient is an alternative statement of the same theorem.

theorem nat.modeq.pow_totient {x n : } (h : x.coprime n) :
x ^ n.totient 1 [MOD n]

The Fermat-Euler totient theorem. zmod.pow_totient is an alternative statement of the same theorem.

theorem card_eq_pow_finrank {K : Type u_1} {V : Type u_3} [fintype K] [ V] [fintype V] :
@[simp]
theorem zmod.pow_card {p : } [fact (nat.prime p)] (x : zmod p) :
x ^ p = x

A variation on Fermat's little theorem. See zmod.pow_card_sub_one_eq_one

@[simp]
theorem zmod.pow_card_pow {n p : } [fact (nat.prime p)] (x : zmod p) :
x ^ p ^ n = x
@[simp]
theorem zmod.frobenius_zmod (p : ) [fact (nat.prime p)] :
@[simp]
theorem zmod.card_units (p : ) [fact (nat.prime p)] :
= p - 1
theorem zmod.units_pow_card_sub_one_eq_one (p : ) [fact (nat.prime p)] (a : (zmod p)ˣ) :
a ^ (p - 1) = 1

Fermat's Little Theorem: for every unit a of zmod p, we have a ^ (p - 1) = 1.

theorem zmod.pow_card_sub_one_eq_one {p : } [fact (nat.prime p)] {a : zmod p} (ha : a 0) :
a ^ (p - 1) = 1

Fermat's Little Theorem: for all nonzero a : zmod p, we have a ^ (p - 1) = 1.

theorem zmod.order_of_units_dvd_card_sub_one {p : } [fact (nat.prime p)] (u : (zmod p)ˣ) :
p - 1
theorem zmod.order_of_dvd_card_sub_one {p : } [fact (nat.prime p)] {a : zmod p} (ha : a 0) :
p - 1
theorem zmod.expand_card {p : } [fact (nat.prime p)] (f : polynomial (zmod p)) :
p) f = f ^ p
theorem int.modeq.pow_card_sub_one_eq_one {p : } (hp : nat.prime p) {n : } (hpn : p) :
n ^ (p - 1) 1 [ZMOD p]

Fermat's Little Theorem: for all a : ℤ coprime to p, we have a ^ (p - 1) ≡ 1 [ZMOD p].

theorem finite_field.is_square_of_char_two {F : Type u_3} [field F] [finite F] (hF : = 2) (a : F) :

In a finite field of characteristic 2, all elements are squares.

theorem finite_field.exists_nonsquare {F : Type u_3} [field F] [finite F] (hF : 2) :
(a : F),

In a finite field of odd characteristic, not every element is a square.

theorem finite_field.even_card_iff_char_two {F : Type u_3} [field F] [fintype F] :
= 2 = 0

The finite field F has even cardinality iff it has characteristic 2.

theorem finite_field.even_card_of_char_two {F : Type u_3} [field F] [fintype F] (hF : = 2) :
= 0
theorem finite_field.odd_card_of_char_ne_two {F : Type u_3} [field F] [fintype F] (hF : 2) :
= 1
theorem finite_field.pow_dichotomy {F : Type u_3} [field F] [fintype F] (hF : 2) {a : F} (ha : a 0) :
a ^ / 2) = 1 a ^ / 2) = -1

If F has odd characteristic, then for nonzero a : F, we have that a ^ (#F / 2) = ±1.

theorem finite_field.unit_is_square_iff {F : Type u_3} [field F] [fintype F] (hF : 2) (a : Fˣ) :
a ^ / 2) = 1

A unit a of a finite field F of odd characteristic is a square if and only if a ^ (#F / 2) = 1.

theorem finite_field.is_square_iff {F : Type u_3} [field F] [fintype F] (hF : 2) {a : F} (ha : a 0) :
a ^ / 2) = 1

A non-zero a : F is a square if and only if a ^ (#F / 2) = 1.