Documentation

Mathlib.FieldTheory.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 RingTheory.IntegralDomain 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.fieldOfDomain).

Main results #

  1. Fintype.card_units: The unit group of a finite field 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. FiniteField.card: The cardinality q is a power of the characteristic of K. See FiniteField.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 can be inferred from Fintype K in the presence of DecidableEq K, in this file we take the Fintype argument directly to reduce the chance of typeclass diamonds, as Fintype carries data.

theorem FiniteField.card_image_polynomial_eval {R : Type u_2} [CommRing R] [IsDomain R] [DecidableEq R] [Fintype R] {p : Polynomial R} (hp : 0 < p.degree) :
Fintype.card R p.natDegree * (Finset.image (fun (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 FiniteField.exists_root_sum_quadratic {R : Type u_2} [CommRing R] [IsDomain R] [Fintype R] {f : Polynomial R} {g : Polynomial R} (hf2 : f.degree = 2) (hg2 : g.degree = 2) (hR : Fintype.card R % 2 = 1) :
∃ (a : R) (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 FiniteField.sum_subgroup_units_eq_zero {K : Type u_1} [Ring K] [NoZeroDivisors K] {G : Subgroup Kˣ} [Fintype G] (hg : G ) :
x : G, x = 0

The sum of a nontrivial subgroup of the units of a field is zero.

@[simp]
theorem FiniteField.sum_subgroup_units {K : Type u_1} [Ring K] [NoZeroDivisors K] {G : Subgroup Kˣ} [Fintype G] [Decidable (G = )] :
x : G, x = if G = then 1 else 0

The sum of a subgroup of the units of a field is 1 if the subgroup is trivial and 1 otherwise

@[simp]
theorem FiniteField.sum_subgroup_pow_eq_zero {K : Type u_1} [CommRing K] [NoZeroDivisors K] {G : Subgroup Kˣ} [Fintype G] {k : } (k_pos : k 0) (k_lt_card_G : k < Fintype.card G) :
x : G, x ^ k = 0
theorem FiniteField.pow_card_sub_one_eq_one {K : Type u_1} [GroupWithZero K] [Fintype K] (a : K) (ha : a 0) :
a ^ (Fintype.card K - 1) = 1
theorem FiniteField.pow_card {K : Type u_1} [GroupWithZero K] [Fintype K] (a : K) :
theorem FiniteField.pow_card_pow {K : Type u_1} [GroupWithZero K] [Fintype K] (n : ) (a : K) :
a ^ Fintype.card K ^ n = a
theorem FiniteField.card (K : Type u_1) [Field K] [Fintype K] (p : ) [CharP K p] :
∃ (n : ℕ+), Nat.Prime p Fintype.card K = p ^ n
theorem FiniteField.card' (K : Type u_1) [Field K] [Fintype K] :
∃ (p : ) (n : ℕ+), Nat.Prime p Fintype.card K = p ^ n
theorem FiniteField.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 FiniteField.sum_pow_units (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (i : ) :
x : Kˣ, x ^ i = if Fintype.card K - 1 i then -1 else 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 FiniteField.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 FiniteField.X_pow_card_sub_X_natDegree_eq (K' : Type u_3) [Field K'] {p : } (hp : 1 < p) :
(Polynomial.X ^ p - Polynomial.X).natDegree = p
theorem FiniteField.X_pow_card_pow_sub_X_natDegree_eq (K' : Type u_3) [Field K'] {p : } {n : } (hn : n 0) (hp : 1 < p) :
(Polynomial.X ^ p ^ n - Polynomial.X).natDegree = p ^ n
theorem FiniteField.X_pow_card_sub_X_ne_zero (K' : Type u_3) [Field K'] {p : } (hp : 1 < p) :
Polynomial.X ^ p - Polynomial.X 0
theorem FiniteField.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 FiniteField.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
theorem FiniteField.frobenius_pow {K : Type u_1} [Field K] [Fintype K] {p : } [Fact (Nat.Prime p)] [CharP K p] {n : } (hcard : Fintype.card K = p ^ n) :
frobenius K p ^ n = 1
theorem ZMod.sq_add_sq (p : ) [hp : Fact (Nat.Prime p)] (x : ZMod p) :
∃ (a : ZMod p) (b : ZMod p), a ^ 2 + b ^ 2 = x
theorem Nat.sq_add_sq_zmodEq (p : ) [Fact (Nat.Prime p)] (x : ) :
∃ (a : ) (b : ), a p / 2 b p / 2 a ^ 2 + b ^ 2 x [ZMOD p]

If p is a prime natural number and x is an integer number, then there exist natural numbers a ≤ p / 2 and b ≤ p / 2 such that a ^ 2 + b ^ 2 ≡ x [ZMOD p]. This is a version of ZMod.sq_add_sq with estimates on a and b.

theorem Nat.sq_add_sq_modEq (p : ) [Fact (Nat.Prime p)] (x : ) :
∃ (a : ) (b : ), a p / 2 b p / 2 a ^ 2 + b ^ 2 x [MOD p]

If p is a prime natural number and x is a natural number, then there exist natural numbers a ≤ p / 2 and b ≤ p / 2 such that a ^ 2 + b ^ 2 ≡ x [MOD p]. This is a version of ZMod.sq_add_sq with estimates on a and b.

theorem CharP.sq_add_sq (R : Type u_3) [CommRing R] [IsDomain R] (p : ) [NeZero p] [CharP R 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.

instance instFiniteZModUnits (n : ) :

For each n ≥ 0, the unit group of ZMod n is finite.

Equations
  • =
@[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.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.pow_card_sub_one {p : } [Fact (Nat.Prime p)] (a : ZMod p) :
a ^ (p - 1) = if a 0 then 1 else 0
theorem ZMod.orderOf_dvd_card_sub_one {p : } [Fact (Nat.Prime p)] {a : ZMod p} (ha : a 0) :
orderOf a p - 1
theorem ZMod.expand_card {p : } [Fact (Nat.Prime p)] (f : Polynomial (ZMod p)) :
(Polynomial.expand (ZMod p) p) f = f ^ p
theorem Int.ModEq.pow_card_sub_one_eq_one {p : } (hp : Nat.Prime p) {n : } (hpn : IsCoprime 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].

theorem FiniteField.isSquare_of_char_two {F : Type u_3} [Field F] [Finite F] (hF : ringChar F = 2) (a : F) :

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

theorem FiniteField.exists_nonsquare {F : Type u_3} [Field F] [Finite F] (hF : ringChar F 2) :
∃ (a : F), ¬IsSquare a

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

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

theorem FiniteField.even_card_of_char_two {F : Type u_3} [Field F] [Fintype F] (hF : ringChar F = 2) :
theorem FiniteField.pow_dichotomy {F : Type u_3} [Field F] [Fintype F] (hF : ringChar F 2) {a : F} (ha : a 0) :
a ^ (Fintype.card F / 2) = 1 a ^ (Fintype.card F / 2) = -1

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

theorem FiniteField.unit_isSquare_iff {F : Type u_3} [Field F] [Fintype F] (hF : ringChar F 2) (a : Fˣ) :

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

theorem FiniteField.isSquare_iff {F : Type u_3} [Field F] [Fintype F] (hF : ringChar F 2) {a : F} (ha : a 0) :

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