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 Kˣ can be inferred from Fintype K in the presence of DecidableEq K, in this file we take the Fintype Kˣ 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 < Polynomial.degree p) : Fintype.card R ≤ Polynomial.natDegree p * Finset.card (Finset.image (fun x => Polynomial.eval x p) Finset.univ)

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 : Polynomial.degree f = 2) (hg2 : Polynomial.degree g = 2) (hR : Fintype.card R % 2 = 1) : ∃ a b, 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.prod_univ_units_id_eq_neg_one {K : Type u_1} [CommRing K] [IsDomain K] [Fintype Kˣ] : (Finset.prod Finset.univ fun x => x) = -1

theorem FiniteField.card_cast_subgroup_card_ne_zero {K : Type u_1} [Ring K] [NoZeroDivisors K] [Nontrivial K] (G : Subgroup Kˣ) [Fintype { x // x ∈ G }] : ↑(Fintype.card { x // x ∈ G }) ≠ 0

theorem FiniteField.sum_subgroup_units_eq_zero {K : Type u_1} [Ring K] [NoZeroDivisors K] {G : Subgroup Kˣ} [Fintype { x // x ∈ G }] (hg : G ≠ ⊥) : (Finset.sum Finset.univ fun x => ↑↑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 { x // x ∈ G }] [Decidable (G = ⊥)] : (Finset.sum Finset.univ fun x => ↑↑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 { x // x ∈ G }] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Fintype.card { x // x ∈ G }) : (Finset.sum Finset.univ fun x => ↑↑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) : a ^ Fintype.card K = a

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.cast_card_eq_zero (K : Type u_1) [Field K] [Fintype K] : ↑(Fintype.card K) = 0

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 : ℕ) : (Finset.sum Finset.univ fun x => ↑(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) : (Finset.sum Finset.univ fun x => 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.natDegree (Polynomial.X ^ p - Polynomial.X) = 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.natDegree (Polynomial.X ^ p ^ n - Polynomial.X) = 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.roots (Polynomial.X ^ Fintype.card K - Polynomial.X) = 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 FiniteField.expand_card {K : Type u_1} [Field K] [Fintype K] (f : Polynomial K) : ↑(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, 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 ^ Nat.totient n = 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 : Nat.Coprime x n) : x ^ Nat.totient n ≡ 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] [DivisionRing K] [AddCommGroup V] [Module K V] [Fintype V] : Fintype.card V = Fintype.card K ^ FiniteDimensional.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 = RingHom.id (ZMod p)

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.orderOf_units_dvd_card_sub_one {p : ℕ} [Fact (Nat.Prime p)] (u : (ZMod p)ˣ) : orderOf u ∣ p - 1

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

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, ¬IsSquare a

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

theorem FiniteField.even_card_iff_char_two {F : Type u_3} [Field F] [Fintype F] : ringChar F = 2 ↔ Fintype.card F % 2 = 0

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) : Fintype.card F % 2 = 0

theorem FiniteField.odd_card_of_char_ne_two {F : Type u_3} [Field F] [Fintype F] (hF : ringChar F ≠ 2) : Fintype.card F % 2 = 1

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ˣ) : IsSquare a ↔ a ^ (Fintype.card F / 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 FiniteField.isSquare_iff {F : Type u_3} [Field F] [Fintype F] (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) : IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

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