English
There is an algebra isomorphism between a finite field K and the GaloisField p n whenever their cardinalities agree with p prime.
Русский
Существует алгебраическое изоморфизм между конечным полем K и полем Галуа p^n, если их кардинальности согласованы с простым p.
LaTeX
$$algEquivGaloisField (p) (n) : K ≃ₐ[ZMod p] GaloisField p n$$
Lean4
/-- Uniqueness of finite fields:
Any two finite fields of the same cardinality are (possibly noncanonically) isomorphic -/
def algEquivOfCardEq (p : ℕ) [h_prime : Fact p.Prime] [Algebra (ZMod p) K] [Algebra (ZMod p) K']
(hKK' : Fintype.card K = Fintype.card K') : K ≃ₐ[ZMod p] K' :=
by
have : CharP K p := by rw [← Algebra.charP_iff (ZMod p) K p]; exact ZMod.charP p
have : CharP K' p := by rw [← Algebra.charP_iff (ZMod p) K' p]; exact ZMod.charP p
choose n a hK using FiniteField.card K p
choose n' a' hK' using FiniteField.card K' p
rw [hK, hK'] at hKK'
have hGalK := GaloisField.algEquivGaloisFieldOfFintype p n hK
have hK'Gal := (GaloisField.algEquivGaloisFieldOfFintype p n' hK').symm
rw [Nat.pow_right_injective h_prime.out.one_lt hKK'] at *
exact AlgEquiv.trans hGalK hK'Gal
