algEquivGaloisFieldOfFintype — Mathlib

English

If F is a finite field with cardinality p^n, then the polynomial X^{p^n} - X has splitting field over ZMod p equal to the target field.

Русский

Если F — конечное поле кардинальности p^n, то X^{p^n} - X распадается над ZMod p в поле F.

LaTeX

$$IsSplittingField (ZMod p) K (X ^ p ^ n - X)$$

Lean4

/-- Any finite field is (possibly noncanonically) isomorphic to some Galois field. -/
def algEquivGaloisFieldOfFintype (h : Fintype.card K = p ^ n) : K ≃ₐ[ZMod p] GaloisField p n :=
  haveI := FiniteField.isSplittingField_of_card_eq _ _ h
  IsSplittingField.algEquiv _ _

Похожие утверждения