let p be Prime; :: thesis: for n being non zero Nat
for F1, F2 being GaloisField of p |^ n holds F1,F2 are_isomorphic_over Z/ p
let n be non zero Nat; :: thesis: for F1, F2 being GaloisField of p |^ n holds F1,F2 are_isomorphic_over Z/ p
let F1, F2 be GaloisField of p |^ n; :: thesis: F1,F2 are_isomorphic_over Z/ p
A: F1 is SplittingField of X^ ((p |^ n),(Z/ p)) by Gsplit;
F2 is SplittingField of X^ ((p |^ n),(Z/ p)) by Gsplit;
hence F1,F2 are_isomorphic_over Z/ p by A, FIELD_8:58; :: thesis: verum