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)