GaloisField — Mathlib

English

If p is prime and n > 0, then the dimension of GaloisField(p,n) as a vector space over ZMod(p) is n.

Русский

Пусть p — простое число и n > 0. Тогда размерность GaloisField(p,n) как векторного пространства над ZMod(p) равна n.

LaTeX

$$Module.finrank (ZMod p) (GaloisField p n) = n$$

Lean4

/-- A finite field with `p ^ n` elements.
Every field with the same cardinality is (non-canonically)
isomorphic to this field. -/
def GaloisField :=
  SplittingField (X ^ p ^ n - X : (ZMod p)[X])
deriving Inhabited, Field, CharP _ p, Algebra (ZMod p), Finite, FiniteDimensional (ZMod p),
  IsSplittingField (ZMod p) _ (X ^ p ^ n - X)

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