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.

Main results

Every finite integral domain is a field (field_of_integral_domain).
The unit group of a finite field is a cyclic group of order q - 1. (finite_field.is_cyclic and card_units)
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.

source

theorem finite_field.card_image_polynomial_eval {R : Type u_2} [integral_domain R] [decidable_eq R] [fintype R] {p : polynomial R} :

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

source

theorem finite_field.exists_root_sum_quadratic {R : Type u_2} [integral_domain R] [fintype R] {f g : polynomial R} :

f.degree = 2 → g.degree = 2 → 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.

source

theorem finite_field.card_units {K : Type u_1} [field K] [fintype K] :

fintype.card (units K) = fintype.card K - 1

source

theorem finite_field.prod_univ_units_id_eq_neg_one {K : Type u_1} [field K] [fintype K] :

finset.univ.prod (λ (x : units K), x) = -1

source

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

a ≠ 0 → a ^ (fintype.card K - 1) = 1

source

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

source

theorem finite_field.card' {K : Type u_1} [field K] [fintype K] :

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

source

@[simp]

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

↑(fintype.card K) = 0

source

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

source

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

finset.univ.sum (λ (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.

source