equivZmodP — Mathlib

English

There is an algebra equivalence between GaloisField(p,1) and ZMod(p).

Русский

Существует алгебраическое эквивалентное отображение между GaloisField(p,1) и ZMod(p).

LaTeX

$$equivZmodP : GaloisField p 1 ≃ₐ[ZMod p] ZMod p$$

Lean4

/-- A Galois field with exponent 1 is equivalent to `ZMod` -/
def equivZmodP : GaloisField p 1 ≃ₐ[ZMod p] ZMod p :=
  have h : (X ^ p ^ 1 : (ZMod p)[X]) = X ^ Fintype.card (ZMod p) := by rw [pow_one, ZMod.card p]
  have inst : IsSplittingField (ZMod p) (ZMod p) (X ^ p ^ 1 - X) := by rw [h]; infer_instance
  (@IsSplittingField.algEquiv _ (ZMod p) _ _ _ (X ^ p ^ 1 - X : (ZMod p)[X]) inst).symm

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