let p be Prime; :: thesis: for n being non zero Nat
for F being GaloisField of p |^ n holds deg (F,(Z/ p)) = n
let n be non zero Nat; :: thesis: for F being GaloisField of p |^ n holds deg (F,(Z/ p)) = n
let F be GaloisField of p |^ n; :: thesis: deg (F,(Z/ p)) = n
set V = VecSp (F,(Z/ p));
[#] (VecSp (F,(Z/ p))) = the carrier of F by FIELD_4:def 6;
then C: VecSp (F,(Z/ p)) is finite-dimensional by RANKNULL:4;
consider T being linear-transformation of (VecSp (F,(Z/ p))),((Z/ p) ^* (dim (VecSp (F,(Z/ p))))) such that
E: T is bijective by C, VECTSP13:30, VECTSP13:def 10;
F: dom T = the carrier of (VecSp (F,(Z/ p))) by FUNCT_2:def 1;
G: rng T = the carrier of ((Z/ p) ^* (dim (VecSp (F,(Z/ p))))) by E, FUNCT_2:def 3;
card (dom T) = card (rng T) by E, CARD_1:70;
then A: card the carrier of (VecSp (F,(Z/ p))) = (card (Z/ p)) |^ (dim (VecSp (F,(Z/ p)))) by F, G, VECTSP13:31
.= p |^ (dim (VecSp (F,(Z/ p)))) by fresh3a ;
card the carrier of (VecSp (F,(Z/ p))) = order F by FIELD_4:def 6
.= p |^ n by defGal ;
then dim (VecSp (F,(Z/ p))) = n by A, lemp;
hence deg (F,(Z/ p)) = n by C, FIELD_4:def 7; :: thesis: verum