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 (field_of_integral_domain).

Main results

  1. 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.

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} [integral_domain R] [fintype R] {f g : polynomial R} (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.card_units {K : Type u_1} [field K] [fintype K] :

theorem finite_field.prod_univ_units_id_eq_neg_one {K : Type u_1} [field K] [fintype K] :
∏ (x : units K), x = -1

theorem finite_field.pow_card_sub_one_eq_one {K : Type u_1} [field K] [fintype K] (a : K) (ha : a 0) :
a ^ (fintype.card K - 1) = 1

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

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

theorem finite_field.forall_pow_eq_one_iff (K : Type u_1) [field K] [fintype K] (i : ) :
(∀ (x : units K), x ^ i = 1) fintype.card K - 1 i

theorem finite_field.sum_pow_units (K : Type u_1) [field K] [fintype K] (i : ) :
∑ (x : units 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.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 : polynomial K) :

theorem zmod.sum_two_squares (p : ) [hp : fact (nat.prime p)] (x : zmod p) :
∃ (a b : zmod p), a ^ 2 + b ^ 2 = x

theorem char_p.sum_two_squares (R : Type u_1) [integral_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 : units (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.

@[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.frobenius_zmod (p : ) [hp : fact (nat.prime p)] :

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

theorem zmod.units_pow_card_sub_one_eq_one (p : ) [fact (nat.prime p)] (a : units (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 : polynomial (zmod p)) :