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 < 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 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.prod_univ_units_id_eq_neg_one {K : Type u_1} [CommRing K] [IsDomain K] [Fintype Kˣ] : ∏ x : Kˣ, x = -1

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

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

The cardinality q is a power of the characteristic of K.

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.isPrimePow_card (K : Type u_1) [Field K] [Fintype K] : IsPrimePow (Fintype.card K)

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 : ℕ) : ∑ 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.

def FiniteField.frobeniusAlgHom (K : Type u_1) (R : Type u_2) [Field K] [Fintype K] [CommRing R] [Algebra K R] : R →ₐ[K] R

If R is an algebra over a finite field K, the Frobenius K-algebra endomorphism of R is given by raising every element of R to its #K-th power.

Equations

• FiniteField.frobeniusAlgHom K R = { toMonoidHom := powMonoidHom (Fintype.card K), map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem FiniteField.frobeniusAlgHom_apply (K : Type u_1) (R : Type u_2) [Field K] [Fintype K] [CommRing R] [Algebra K R] (x✝ : R) : (frobeniusAlgHom K R) x✝ = x✝ ^ Fintype.card K

theorem FiniteField.coe_frobeniusAlgHom (K : Type u_1) (R : Type u_2) [Field K] [Fintype K] [CommRing R] [Algebra K R] : ⇑(frobeniusAlgHom K R) = fun (x : R) => x ^ Fintype.card K

noncomputable def FiniteField.frobeniusAlgEquiv (K : Type u_1) (R : Type u_2) [Field K] [Fintype K] [CommRing R] [Algebra K R] (p : ℕ) [ExpChar R p] [PerfectRing R p] : R ≃ₐ[K] R

If R is a perfect ring and an algebra over a finite field K, the Frobenius K-algebra endomorphism of R is an automorphism.

Equations

• FiniteField.frobeniusAlgEquiv K R p = AlgEquiv.ofBijective (FiniteField.frobeniusAlgHom K R) ⋯

@[simp]

theorem FiniteField.frobeniusAlgEquiv_apply (K : Type u_1) (R : Type u_2) [Field K] [Fintype K] [CommRing R] [Algebra K R] (p : ℕ) [ExpChar R p] [PerfectRing R p] (a : R) : (frobeniusAlgEquiv K R p) a = a ^ Fintype.card K

@[simp]

theorem FiniteField.frobeniusAlgEquiv_symm_apply (K : Type u_1) (R : Type u_2) [Field K] [Fintype K] [CommRing R] [Algebra K R] (p : ℕ) [ExpChar R p] [PerfectRing R p] (b : R) : (frobeniusAlgEquiv K R p).symm b = Function.surjInv ⋯ b

noncomputable def FiniteField.frobeniusAlgEquivOfAlgebraic (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] : L ≃ₐ[K] L

If L/K is an algebraic extension of a finite field, the Frobenius K-algebra endomorphism of L is an automorphism.

Equations

• FiniteField.frobeniusAlgEquivOfAlgebraic K L = (Algebra.IsAlgebraic.algEquivEquivAlgHom K L).symm (FiniteField.frobeniusAlgHom K L)

@[simp]

theorem FiniteField.frobeniusAlgEquivOfAlgebraic_apply (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (a : L) : (frobeniusAlgEquivOfAlgebraic K L) a = a ^ Fintype.card K

@[simp]

theorem FiniteField.frobeniusAlgEquivOfAlgebraic_symm_apply (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (b : L) : (frobeniusAlgEquivOfAlgebraic K L).symm b = Function.surjInv ⋯ b

theorem FiniteField.coe_frobeniusAlgEquivOfAlgebraic (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] : ⇑(frobeniusAlgEquivOfAlgebraic K L) = fun (x : L) => x ^ Fintype.card K

theorem FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (n : ℕ) : (⇑(frobeniusAlgEquivOfAlgebraic K L))^[n] = fun (x : L) => x ^ Fintype.card K ^ n

theorem FiniteField.orderOf_frobeniusAlgHom (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Finite L] : orderOf (frobeniusAlgHom K L) = Module.finrank K L

theorem FiniteField.orderOf_frobeniusAlgEquivOfAlgebraic (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Finite L] : orderOf (frobeniusAlgEquivOfAlgebraic K L) = Module.finrank K L

theorem FiniteField.bijective_frobeniusAlgHom_pow (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Finite L] : Function.Bijective fun (n : Fin (Module.finrank K L)) => frobeniusAlgHom K L ^ ↑n

theorem FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Finite L] : Function.Bijective fun (n : Fin (Module.finrank K L)) => frobeniusAlgEquivOfAlgebraic K L ^ ↑n

instance FiniteField.instIsCyclicAlgEquivOfFinite (K : Type u_4) (L : Type u_5) [Finite L] [Field K] [Field L] [Algebra K L] : IsCyclic (L ≃ₐ[K] L)

theorem FiniteField.minpoly_frobeniusAlgHom (K : Type u_1) [Field K] [Fintype K] (L : Type u_3) [Field L] [Algebra K L] [Finite L] : minpoly K (frobeniusAlgHom K L).toLinearMap = Polynomial.X ^ Module.finrank K L - 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 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 : ZMod p) (b : ZMod p), a ^ 2 + b ^ 2 = x

theorem Nat.sq_add_sq_zmodEq (p : ℕ) [Fact (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 (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) [Ring 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 : ℕ) : Finite (ZMod n)ˣ

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

instance ZMod.instSubsingletonSubfield {p : ℕ} [Fact (Nat.Prime p)] : Subsingleton (Subfield (ZMod p))

theorem ZMod.fieldRange_castHom_eq_bot {K : Type u_1} (p : ℕ) [Fact (Nat.Prime p)] [DivisionRing K] [CharP K p] : (castHom ⋯ K).fieldRange = ⊥

@[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 {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (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.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_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 Int.prime_dvd_pow_sub_one {p : ℕ} (hp : Nat.Prime p) {n : ℤ} (hpn : IsCoprime n ↑p) : ↑p ∣ n ^ (p - 1) - 1

theorem Int.ModEq.pow_prime_eq_self {p : ℕ} (hp : Nat.Prime p) (n : ℤ) : n ^ p ≡ n [ZMOD ↑p]

theorem Int.prime_dvd_pow_self_sub {p : ℕ} (hp : Nat.Prime p) (n : ℤ) : ↑p ∣ n ^ p - n

theorem Int.ModEq.pow_eq_pow {p x y : ℕ} (hp : Nat.Prime p) (h : p - 1 ∣ x - y) (hxy : y ≤ x) (hy : 0 < y) (n : ℤ) : n ^ x ≡ n ^ y [ZMOD ↑p]

theorem Nat.ModEq.pow_card_sub_one_eq_one {p : ℕ} (hp : Prime p) {n : ℕ} (hpn : n.Coprime p) : n ^ (p - 1) ≡ 1 [MOD p]

Fermat's Little Theorem: for all n : ℕ coprime to p, we have n ^ (p - 1) ≡ 1 [MOD p].

theorem Nat.pow_card_sub_one_sub_one_mod_card {p : ℕ} (hp : Prime p) {n : ℕ} (hpn : n.Coprime p) : (n ^ (p - 1) - 1) % p = 0

Fermat's Little Theorem: for all n : ℕ coprime to p, we have (n ^ (p - 1) - 1) % p = 0.

theorem pow_pow_modEq_one (p m a : ℕ) : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]

theorem ZMod.eq_one_or_isUnit_sub_one {n p k : ℕ} [Fact (Nat.Prime p)] (hn : n = p ^ k) (a : ZMod n) (ha : (orderOf a).Coprime n) : a = 1 ∨ IsUnit (a - 1)

theorem mem_bot_iff_intCast (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_4) [DivisionRing K] [CharP K p] {x : K} : x ∈ ⊥ ↔ ∃ (n : ℤ), ↑n = x

theorem Subfield.card_bot (F : Type u_3) [Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] : Nat.card ↥⊥ = p

def Subfield.fintypeBot (F : Type u_3) [Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] : Fintype ↥⊥

The prime subfield is finite.

Equations

• Subfield.fintypeBot F p = Fintype.subtype (Finset.map { toFun := ⇑(ZMod.castHom ⋯ F), inj' := ⋯ } Finset.univ) ⋯

theorem Subfield.roots_X_pow_char_sub_X_bot (F : Type u_3) [Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] : (Polynomial.X ^ p - Polynomial.X).roots = Finset.univ.val

theorem Subfield.splits_bot (F : Type u_3) [Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] : Polynomial.Splits (RingHom.id ↥⊥) (Polynomial.X ^ p - Polynomial.X)

theorem Subfield.mem_bot_iff_pow_eq_self (F : Type u_3) [Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] {x : F} : x ∈ ⊥ ↔ x ^ p = x

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 : F), ¬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.