let p be Prime; :: thesis: for F being p -characteristic Field
for a being Element of F st not a in F |^ p holds
( X^ (p,a) is irreducible & X^ (p,a) is inseparable )
let F be p -characteristic Field; :: thesis: for a being Element of F st not a in F |^ p holds
( X^ (p,a) is irreducible & X^ (p,a) is inseparable )
let a be Element of F; :: thesis: ( not a in F |^ p implies ( X^ (p,a) is irreducible & X^ (p,a) is inseparable ) )
assume A0: not a in F |^ p ; :: thesis: ( X^ (p,a) is irreducible & X^ (p,a) is inseparable )
the carrier of (F |^ p) = { (a |^ p) where a is Element of F : verum } by deffp;
then for b being Element of F holds not b |^ p = a by A0;
hence X^ (p,a) is irreducible by pirred; :: thesis: X^ (p,a) is inseparable
consider E being FieldExtension of F such that
A2: X^ (p,a) is_with_roots_in E by FIELD_5:30;
consider b being Element of E such that
A3: b is_a_root_of X^ (p,a),E by A2, FIELD_4:def 3;
F is Subfield of E by FIELD_4:7;
then the carrier of F c= the carrier of E by EC_PF_1:def 1;
then reconsider aE = a as Element of E ;
A4: X^ (p,a) = X^ (p,aE) by split2;
0. E = Ext_eval ((X^ (p,a)),b) by A3, FIELD_4:def 2
.= eval ((X^ (p,aE)),b) by split2, FIELD_4:26 ;
then b is_a_root_of X^ (p,aE) ;
then b |^ p = aE by split1;
then X^ (p,aE) = (X- b) |^ p by split0
.= (X- b) `^ p ;
then p = multiplicity ((X^ (p,aE)),b) by ro0
.= multiplicity ((X^ (p,a)),b) by A4, FIELD_14:def 6 ;
hence X^ (p,a) is inseparable by INT_2:def 4, ThSep02; :: thesis: verum