let p be Prime; :: thesis: for n being non zero Nat
for F being finite Field st card F = p |^ n holds
X^ ((p |^ n),F) is Ppoly of F,([#] the carrier of F)
let n be non zero Nat; :: thesis: for F being finite Field st card F = p |^ n holds
X^ ((p |^ n),F) is Ppoly of F,([#] the carrier of F)
let F be finite Field; :: thesis: ( card F = p |^ n implies X^ ((p |^ n),F) is Ppoly of F,([#] the carrier of F) )
assume AS: card F = p |^ n ; :: thesis: X^ ((p |^ n),F) is Ppoly of F,([#] the carrier of F)
consider n1 being non zero Nat such that
A: card F = (Char F) |^ n1 by FIELD_15:92;
Char F = p by A, AS, lemp;
then H: F is p -characteristic by RING_3:def 6;
set q = X^ ((p |^ n),F);
F is SplittingField of X^ ((p |^ n),(PrimeField F)) by AS, split;
then X^ ((p |^ n),(PrimeField F)) splits_in F by FIELD_8:def 1;
then consider x being non zero Element of F, v being Ppoly of F such that
I: X^ ((p |^ n),(PrimeField F)) = x * v by FIELD_4:def 5;
F is FieldExtension of PrimeField F by FIELD_4:7;
then E: X^ ((p |^ n),F) = X^ ((p |^ n),(PrimeField F)) by Xm;
then consider a being non zero Element of F, q1 being Ppoly of F such that
A: X^ ((p |^ n),F) = a * q1 by I;
B: a = a * (1. F)
.= a * (LC q1) by RING_5:50
.= LC (X^ ((p |^ n),F)) by A, RING_5:5
.= 1. F by Lm13 ;

C: now :: thesis: for a being Element of F st a is_a_root_of X^ ((p |^ n),F) holds
multiplicity ((X^ ((p |^ n),F)),a) = 1

let a be Element of F; :: thesis: ( a is_a_root_of X^ ((p |^ n),F) implies multiplicity ((X^ ((p |^ n),F)),a) = 1 )
assume D1: a is_a_root_of X^ ((p |^ n),F) ; :: thesis: multiplicity ((X^ ((p |^ n),F)),a) = 1
reconsider F1 = F as FieldExtension of F by FIELD_4:6;
reconsider a1 = a as Element of F1 ;
0. F = Ext_eval ((X^ ((p |^ n),F)),a1) by D1, FIELD_4:26;
then D2: a1 is_a_root_of X^ ((p |^ n),F),F1 by FIELD_4:def 2;
thus multiplicity ((X^ ((p |^ n),F)),a) = multiplicity ((X^ ((p |^ n),F)),a1) by FIELD_14:def 6
.= 1 by D2, H, E, I, FIELD_4:def 5, FIELD_15:75 ; :: thesis: verum

end;

Roots q1 = the carrier of F by AS, H, A, B, thX1ee
.= [#] the carrier of F by SUBSET_1:def 3 ;
hence X^ ((p |^ n),F) is Ppoly of F,([#] the carrier of F) by A, B, C, FIELD_14:30; :: thesis: verum