mathlib documentation

field_theory.finite.basic

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 cardinality q - 1.
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
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 : R[X]} (hp : 0 < p.degree) :

fintype.card R ≤ (p.nat_degree) * (finset.image (λ (x : R), polynomial.eval x p) finset.univ).card

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 : R[X]} (hf2 : f.degree = 2) (hg2 : g.degree = 2) (hR : fintype.card R % 2 = 1) :

∃ (a b : R), polynomial.eval a f + polynomial.eval b g = 0

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

theorem finite_field.prod_univ_units_id_eq_neg_one {K : Type u_1} [comm_ring K] [is_domain K] [fintype Kˣ] :

∏ (x : Kˣ), x = -1

theorem finite_field.pow_card_sub_one_eq_one {K : Type u_1} [group_with_zero K] [fintype K] (a : K) (ha : a ≠ 0) :

a ^ (fintype.card K - 1) = 1

theorem finite_field.pow_card {K : Type u_1} [group_with_zero K] [fintype K] (a : K) :

a ^ fintype.card K = a

theorem finite_field.pow_card_pow {K : Type u_1} [group_with_zero K] [fintype K] (n : ℕ) (a : K) :

a ^ fintype.card K ^ n = a

theorem finite_field.card (K : Type u_1) [field K] [fintype K] (p : ℕ) [char_p K p] :

∃ (n : ℕ+), nat.prime p ∧ fintype.card K = p ^ ↑n

theorem finite_field.card' (K : Type u_1) [field K] [fintype K] :

∃ (p : ℕ) (n : ℕ+), nat.prime p ∧ fintype.card K = p ^ ↑n

@[simp]

theorem finite_field.cast_card_eq_zero (K : Type u_1) [field K] [fintype K] :

↑(fintype.card K) = 0

theorem finite_field.forall_pow_eq_one_iff (K : Type u_1) [field K] [fintype K] (i : ℕ) :

(∀ (x : Kˣ), x ^ i = 1) ↔ fintype.card K - 1 ∣ i

theorem finite_field.sum_pow_units (K : Type u_1) [field K] [fintype K] [fintype Kˣ] (i : ℕ) :

∑ (x : Kˣ), ↑x ^ i = ite (fintype.card K - 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 < fintype.card K - 1) :

∑ (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) :

(polynomial.X ^ p - polynomial.X).nat_degree = 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) :

(polynomial.X ^ p ^ n - polynomial.X).nat_degree = p ^ n

theorem finite_field.X_pow_card_sub_X_ne_zero (K' : Type u_3) [field K'] {p : ℕ} (hp : 1 < p) :

polynomial.X ^ p - polynomial.X ≠ 0

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) :

polynomial.X ^ p ^ n - polynomial.X ≠ 0

theorem finite_field.roots_X_pow_card_sub_X (K : Type u_1) [field K] [fintype K] :

(polynomial.X ^ fintype.card K - polynomial.X).roots = finset.univ.val

@[protected, instance]

def finite_field.has_sub.sub.polynomial.is_splitting_field (K : Type u_1) [field K] [fintype K] (p : ℕ) [fact (nat.prime p)] [char_p K p] :

polynomial.is_splitting_field (zmod p) K (polynomial.X ^ fintype.card K - polynomial.X)

theorem finite_field.frobenius_pow {K : Type u_1} [field K] [fintype K] {p : ℕ} [fact (nat.prime p)] [char_p K p] {n : ℕ} (hcard : fintype.card K = p ^ n) :

frobenius K p ^ n = 1

theorem finite_field.expand_card {K : Type u_1} [field K] [fintype K] (f : K[X]) :

⇑(polynomial.expand K (fintype.card K)) f = f ^ fintype.card 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 : ℕ) [fact (0 < p)] [char_p R p] (x : ℤ) :

∃ (a b : ℕ), ↑a ^ 2 + ↑b ^ 2 = ↑x

@[simp]

theorem zmod.pow_totient {n : ℕ} [fact (0 < 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] [division_ring K] [add_comm_group V] [module K V] [fintype V] :

fintype.card V = fintype.card K ^ finite_dimensional.finrank K 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)] :

frobenius (zmod p) p = ring_hom.id (zmod p)

@[simp]

theorem zmod.card_units (p : ℕ) [fact (nat.prime p)] :

fintype.card (zmod 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.expand_card {p : ℕ} [fact (nat.prime p)] (f : (zmod p)[X]) :

⇑(polynomial.expand (zmod p) p) f = f ^ p

theorem int.modeq.pow_card_sub_one_eq_one {p : ℕ} (hp : nat.prime p) {n : ℤ} (hpn : is_coprime n ↑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].