English
A universal algebraic equivalence exists between ZMod p and GaloisField p n when card(K) = p^n.
Русский
Существуют алгебраические эквиваленты между ZMod p и GaloisField p^n при условии card(K) = p^n.
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 ringEquivOfCardEq (hKK' : Fintype.card K = Fintype.card K') : K ≃+* K' :=
by
choose p _char_p_K using CharP.exists K
choose p' _char_p'_K' using CharP.exists K'
choose n hp hK using FiniteField.card K p
choose n' hp' hK' using FiniteField.card K' p'
have hpp' : p = p' := by
by_contra hne
have h2 := Nat.coprime_pow_primes n n' hp hp' hne
rw [(Eq.congr hK hK').mp hKK', Nat.coprime_self, pow_eq_one_iff (PNat.ne_zero n')] at h2
exact Nat.Prime.ne_one hp' h2
rw [← hpp'] at _char_p'_K'
haveI := fact_iff.2 hp
letI : Algebra (ZMod p) K := ZMod.algebra _ _
letI : Algebra (ZMod p) K' := ZMod.algebra _ _
exact ↑(algEquivOfCardEq p hKK')
