English
Given two finite fields with the same cardinality, there exists an algebra isomorphism between them over ZMod p.
Русский
Для двух конечных полей с одинаковой кардинальностью существует алгебраическое изоморфизм между ними над ZMod p.
LaTeX
$$algEquivOfCardEq (hKK' : Fintype.card K = Fintype.card K') : K ≃ₐ[ZMod p] K'$$
Lean4
theorem algebraMap_norm_eq_pow {x : K'} :
algebraMap K K' (Algebra.norm K x) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1)) :=
by
have := Finite.of_injective _ (algebraMap K K').injective
have := Fintype.ofFinite K
have := Fintype.ofFinite K'
simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms, ←
(bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic,
pow_iterate, Finset.prod_pow_eq_pow_sum, Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ←
Module.card_eq_pow_finrank]
