:: Separable Polynomials and Separable Extensions
:: by Christoph Schwarzweller
::
:: Received June 18, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users


registration
let R be Ring;
let k be non zero Nat;
reduce (0. R) |^ k to 0. R;
reducibility
(0. R) |^ k = 0. R
proof end;
end;

registration
let R be Ring;
let k be Nat;
reduce (1. R) |^ k to 1. R;
reducibility
(1. R) |^ k = 1. R
proof end;
end;

registration
let p be Prime;
cluster non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID K858() -homomorphic factorial p -characteristic for doubleLoopStr ;
existence
ex b1 being Field st
( b1 is finite & b1 is p -characteristic )
proof end;
end;

registration
let F be finite Field;
cluster Char F -> prime ;
coherence
Char F is prime
proof end;
end;

registration
let R be non degenerated Ring;
cluster monic -> non zero for Element of the carrier of (Polynom-Ring R);
coherence
for b1 being Element of the carrier of (Polynom-Ring R) st b1 is monic holds
not b1 is zero ;
end;

definition
let F be Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
let a be non zero Element of F;
:: original: *
redefine func a * p -> non constant Element of the carrier of (Polynom-Ring F);
coherence
a * p is non constant Element of the carrier of (Polynom-Ring F)
proof end;
end;

theorem Lm3b: :: FIELD_15:1
for n being Nat
for m being non zero Nat holds
( n / m is Nat iff m divides n )
proof end;

theorem :: FIELD_15:2
for p being Prime
for n, a, b being Nat st p divides a & not p divides b & n = a / b holds
p divides n
proof end;

theorem gcdp: :: FIELD_15:3
for p being Prime
for n being non zero Nat st n < p holds
n gcd p = 1
proof end;

theorem CF1: :: FIELD_15:4
for n being non zero Nat
for p being Prime ex k, m being Nat st
( n = m * (p |^ k) & not p divides m )
proof end;

registration
let R be domRing;
let a be non zero Element of R;
let n be Nat;
cluster a |^ n -> non zero ;
coherence
not a |^ n is zero
proof end;
end;

theorem teven: :: FIELD_15:5
for R being Ring
for a being Element of R
for n being even Nat holds (- a) |^ n = a |^ n
proof end;

theorem todd: :: FIELD_15:6
for R being Ring
for a being Element of R
for n being odd Nat holds (- a) |^ n = - (a |^ n)
proof end;

theorem t2: :: FIELD_15:7
for R being 2 -characteristic Ring
for a being Element of R holds - a = a
proof end;

theorem Lm0x: :: FIELD_15:8
for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for i being Integer holds i '*' (0. R) = 0. R
proof end;

registration
let F be finite Field;
cluster MultGroup F -> cyclic ;
coherence
MultGroup F is cyclic
proof end;
end;

theorem MGsub: :: FIELD_15:9
for F being Field
for E being FieldExtension of F holds MultGroup F is Subgroup of MultGroup E
proof end;

theorem MG: :: FIELD_15:10
for R being Skew-Field
for n being Nat
for a being Element of R
for b being Element of (MultGroup R) st a = b holds
a |^ n = b |^ n
proof end;

Th28: for L being non empty ZeroStr
for a being Element of L holds
( (a | L) . 0 = a & ( for n being Nat st n <> 0 holds
(a | L) . n = 0. L ) )
proof end;

theorem BBD: :: FIELD_15:11
for R being Ring
for p being Polynomial of R
for a, b being Element of R holds (a + b) * p = (a * p) + (b * p)
proof end;

theorem :: FIELD_15:12
for R being Ring
for p being Polynomial of R
for a, b being Element of R holds (a * b) * p = a * (b * p)
proof end;

theorem :: FIELD_15:13
for R being Ring
for q being Element of the carrier of (Polynom-Ring R)
for p being Polynomial of R
for n being Nat st p = q holds
(n * (1. R)) * p = n * q
proof end;

theorem BBB: :: FIELD_15:14
for R being Ring
for q being Element of the carrier of (Polynom-Ring R)
for p being Polynomial of R
for n, j being Nat st p = n * q holds
p . j = n * (q . j)
proof end;

theorem ll: :: FIELD_15:15
for F being Field
for a being Element of F
for p being Polynomial of F
for E being FieldExtension of F
for b being Element of E
for q being Polynomial of E st a = b & p = q holds
a * p = b * q
proof end;

theorem :: FIELD_15:16
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring F) holds
( not q divides p or q is unital or q is_associated_to p )
proof end;

theorem lemir: :: FIELD_15:17
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for q being monic Element of the carrier of (Polynom-Ring F) holds
( not q divides p or q = 1_. F or q = NormPolynomial p )
proof end;

theorem R441: :: FIELD_15:18
for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F) holds
( ( p is Unit of (Polynom-Ring F) or ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) ) iff p is reducible )
proof end;

theorem :: FIELD_15:19
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is reducible iff ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) )
proof end;

registration
let R be domRing;
let p be non zero Polynomial of R;
let n be Nat;
cluster p `^ n -> non zero ;
coherence
not p `^ n is zero
proof end;
end;

registration
let F be Field;
let p be non constant Polynomial of F;
let n be non zero Nat;
cluster p `^ n -> non constant ;
coherence
not p `^ n is constant
proof end;
end;

registration
let F be Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
let n be non zero Nat;
cluster p |^ n -> non constant ;
coherence
not p |^ n is constant
proof end;
end;

t1: for R being domRing
for p being non zero Polynomial of R
for n being Nat holds deg (p `^ n) = n * (deg p)
proof end;

registration
let F be Field;
let p be constant Element of the carrier of (Polynom-Ring F);
let n be non zero Nat;
cluster p |^ n -> constant ;
coherence
p |^ n is constant
proof end;
end;

registration
let F be Field;
let p be constant Element of the carrier of (Polynom-Ring F);
let n be non zero Nat;
cluster p `^ n -> constant ;
coherence
p `^ n is constant
proof end;
end;

theorem :: FIELD_15:20
for R being domRing
for p being Polynomial of R
for n being Nat holds LC (p `^ n) = (LC p) |^ n
proof end;

theorem :: FIELD_15:21
for R being domRing
for p being non zero Polynomial of R
for n being Nat holds deg (p `^ n) = n * (deg p) by t1;

t3a: for R being Ring
for p, q being Polynomial of R holds (p *' q) . 0 = (p . 0) * (q . 0)
proof end;

theorem t3: :: FIELD_15:22
for R being commutative Ring
for p being Polynomial of R
for n being non zero Nat holds (p `^ n) . 0 = (p . 0) |^ n
proof end;

t4b: for R being domRing
for a being non zero Element of R holds <%(0. R),a%> = a * <%(0. R),(1. R)%>
proof end;

theorem t4a: :: FIELD_15:23
for R being domRing
for a being non zero Element of R
for n being Nat holds <%(0. R),a%> `^ n = (a |^ n) * (<%(0. R),(1. R)%> `^ n)
proof end;

theorem :: FIELD_15:24
for F being Field
for a being Element of F
for n being Nat holds (a | F) `^ n = (a |^ n) | F
proof end;

theorem DP3: :: FIELD_15:25
for F being Field
for a being non zero Element of F
for n, m being Nat holds (anpoly (a,m)) `^ n = anpoly ((a |^ n),(n * m))
proof end;

t4: for R being domRing
for a being non zero Element of R
for n being non zero Nat
for m being Nat st m <> n holds
(<%(0. R),a%> `^ n) . m = 0. R
proof end;

theorem Lm12a: :: FIELD_15:26
for F being Field
for a being Element of F
for n being Nat holds deg ((X- a) `^ n) = n
proof end;

theorem Lm12b: :: FIELD_15:27
for F being Field
for a being Element of F
for n being non zero Nat holds Roots ((X- a) `^ n) = {a}
proof end;

theorem ro0: :: FIELD_15:28
for F being Field
for a being Element of F
for n being Nat holds multiplicity (((X- a) `^ n),a) = n
proof end;

theorem caBR: :: FIELD_15:29
for F being Field
for a being Element of F
for n being Nat holds card (BRoots ((X- a) `^ n)) = n
proof end;

theorem XYZ: :: FIELD_15:30
for R being non degenerated comRing
for S being comRingExtension of R
for a being Element of R
for b being Element of S
for n being Element of NAT st a = b holds
(X- b) `^ n = (X- a) `^ n
proof end;

ro00: for F being Field
for p being non zero Polynomial of F
for a being Element of F holds deg p >= multiplicity (p,a)
proof end;

theorem ro1: :: FIELD_15:31
for F being Field
for p being monic Polynomial of F
for a being Element of F
for n being Nat holds
( p divides (X- a) `^ n iff ex l being Nat st
( l <= n & p = (X- a) `^ l ) )
proof end;

theorem :: FIELD_15:32
for R being non degenerated comRing
for a, b being Element of R
for n being Nat holds eval (((X+ a) `^ n),b) = (a + b) |^ n
proof end;

theorem sp: :: FIELD_15:33
for F being Field
for a being Element of F
for n being non zero Nat holds (X- a) `^ n splits_in F
proof end;

theorem aXn: :: FIELD_15:34
for F1 being Field
for F2 being b1 -homomorphic Field
for h being Homomorphism of F1,F2
for a being Element of F1
for n being Nat holds (PolyHom h) . ((X- a) `^ n) = (X- (h . a)) `^ n
proof end;

registration
let p be Prime;
cluster non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative p -characteristic -> non degenerated commutative p -characteristic for doubleLoopStr ;
coherence
for b1 being commutative p -characteristic Ring holds not b1 is degenerated
proof end;
end;

theorem Lm0: :: FIELD_15:35
for p being Prime
for R being commutative b1 -characteristic Ring
for a being Element of R holds p * a = 0. R
proof end;

theorem Lm0a: :: FIELD_15:36
for p being Prime
for R being commutative b1 -characteristic Ring
for a being non zero Element of R
for n being non zero Nat st n < p holds
n * a <> 0. R
proof end;

theorem Lm1: :: FIELD_15:37
for p being Prime
for R being commutative b1 -characteristic Ring
for a being Element of R
for n being Nat holds (n * p) * a = 0. R
proof end;

theorem Lm2: :: FIELD_15:38
for p being Prime
for R being commutative b1 -characteristic Ring
for a being Element of R
for n being Nat st p divides n holds
n * a = 0. R
proof end;

theorem Lm2a: :: FIELD_15:39
for p being Prime
for R being commutative b1 -characteristic Ring
for a being non zero Element of R
for n being Nat holds
( p divides n iff n * a = 0. R )
proof end;

theorem fresh: :: FIELD_15:40
for p being Prime
for R being commutative b1 -characteristic Ring
for a, b being Element of R holds (a + b) |^ p = (a |^ p) + (b |^ p)
proof end;

theorem :: FIELD_15:41
for p being Prime
for R being commutative b1 -characteristic Ring
for a, b being Element of R
for i being Nat holds (a + b) |^ (p |^ i) = (a |^ (p |^ i)) + (b |^ (p |^ i))
proof end;

theorem fresh2: :: FIELD_15:42
for p being Prime
for R being commutative b1 -characteristic Ring
for a being Element of R holds - (a |^ p) = (- a) |^ p
proof end;

definition
let p be Prime;
let R be commutative p -characteristic Ring;
func R |^ p -> strict doubleLoopStr means :deffp: :: FIELD_15:def 1
( the carrier of it = { (a |^ p) where a is Element of R : verum } & the addF of it = the addF of R || the carrier of it & the multF of it = the multF of R || the carrier of it & 1. it = 1. R & 0. it = 0. R );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = { (a |^ p) where a is Element of R : verum } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 1. b1 = 1. R & 0. b1 = 0. R )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = { (a |^ p) where a is Element of R : verum } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 1. b1 = 1. R & 0. b1 = 0. R & the carrier of b2 = { (a |^ p) where a is Element of R : verum } & the addF of b2 = the addF of R || the carrier of b2 & the multF of b2 = the multF of R || the carrier of b2 & 1. b2 = 1. R & 0. b2 = 0. R holds
b1 = b2 ;
end;

:: deftheorem deffp defines |^ FIELD_15:def 1 :
for p being Prime
for R being commutative b1 -characteristic Ring
for b3 being strict doubleLoopStr holds
( b3 = R |^ p iff ( the carrier of b3 = { (a |^ p) where a is Element of R : verum } & the addF of b3 = the addF of R || the carrier of b3 & the multF of b3 = the multF of R || the carrier of b3 & 1. b3 = 1. R & 0. b3 = 0. R ) );

registration
let p be Prime;
let R be commutative p -characteristic Ring;
cluster R |^ p -> non degenerated strict ;
coherence
not R |^ p is degenerated
proof end;
end;

theorem Lm11: :: FIELD_15:43
for p being Prime
for R being commutative b1 -characteristic Ring
for a, b being Element of R
for x, y being Element of (R |^ p) st a = x & b = y holds
a + b = x + y
proof end;

Lm10: for p being Prime
for R being commutative b1 -characteristic Ring
for x being Element of (R |^ p) holds x is Element of R
proof end;

theorem Lm12: :: FIELD_15:44
for p being Prime
for R being commutative b1 -characteristic Ring
for a, b being Element of R
for x, y being Element of (R |^ p) st a = x & b = y holds
a * b = x * y
proof end;

registration
let p be Prime;
let R be commutative p -characteristic Ring;
cluster R |^ p -> right_complementable strict Abelian add-associative right_zeroed ;
coherence
( R |^ p is Abelian & R |^ p is add-associative & R |^ p is right_zeroed & R |^ p is right_complementable )
proof end;
end;

registration
let p be Prime;
let R be commutative p -characteristic Ring;
cluster R |^ p -> strict well-unital distributive associative commutative ;
coherence
( R |^ p is commutative & R |^ p is associative & R |^ p is well-unital & R |^ p is distributive )
proof end;
end;

registration
let p be Prime;
let F be p -characteristic Field;
cluster F |^ p -> almost_left_invertible strict ;
coherence
F |^ p is almost_left_invertible
proof end;
end;

registration
let p be Prime;
let R be commutative p -characteristic Ring;
cluster R |^ p -> strict p -characteristic ;
coherence
R |^ p is p -characteristic
proof end;
end;

definition
let p be Prime;
let F be p -characteristic Field;
:: original: |^
redefine func F |^ p -> strict Subfield of F;
coherence
F |^ p is strict Subfield of F
proof end;
end;

Lm10: for L being non empty unital doubleLoopStr
for n being non zero Nat
for a being Element of L holds
( ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . 0 = - a & ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . n = 1. L )
proof end;

Lm11: for L being non empty unital doubleLoopStr
for a being Element of L
for i, n being Nat st i <> 0 & i <> n holds
((0_. L) +* ((0,n) --> ((- a),(1. L)))) . i = 0. L
proof end;

definition
let R be non empty unital doubleLoopStr ;
let a be Element of R;
let n be non zero Nat;
func X^ (n,a) -> sequence of R equals :: FIELD_15:def 2
(0_. R) +* ((0,n) --> ((- a),(1. R)));
coherence
(0_. R) +* ((0,n) --> ((- a),(1. R))) is sequence of R
proof end;
end;

:: deftheorem defines X^ FIELD_15:def 2 :
for R being non empty unital doubleLoopStr
for a being Element of R
for n being non zero Nat holds X^ (n,a) = (0_. R) +* ((0,n) --> ((- a),(1. R)));

registration
let R be non empty unital doubleLoopStr ;
let a be Element of R;
let n be non zero Nat;
cluster X^ (n,a) -> finite-Support ;
coherence
X^ (n,a) is finite-Support ;
end;

Lm12: for R being non degenerated unital doubleLoopStr
for a being Element of R
for n being non zero Nat holds deg (X^ (n,a)) = n
proof end;

Lm13: for R being non degenerated unital doubleLoopStr
for a being Element of R
for n being non zero Nat holds LC (X^ (n,a)) = 1. R
proof end;

registration
let R be non degenerated unital doubleLoopStr ;
let a be Element of R;
let n be non zero Nat;
cluster X^ (n,a) -> non constant monic ;
coherence
( not X^ (n,a) is constant & X^ (n,a) is monic )
proof end;
end;

definition
let R be non degenerated Ring;
let a be Element of R;
let n be non zero Nat;
:: original: X^
redefine func X^ (n,a) -> monic non constant Element of the carrier of (Polynom-Ring R);
coherence
X^ (n,a) is monic non constant Element of the carrier of (Polynom-Ring R)
proof end;
end;

theorem :: FIELD_15:45
for L being non degenerated unital doubleLoopStr
for a being Element of L
for n being non zero Nat holds
( (X^ (n,a)) . 0 = - a & (X^ (n,a)) . n = 1. L & ( for m being Nat st m <> 0 & m <> n holds
(X^ (n,a)) . m = 0. L ) ) by Lm10, Lm11;

theorem :: FIELD_15:46
for R being non degenerated unital doubleLoopStr
for n being non zero Nat
for a being Element of R holds deg (X^ (n,a)) = n by Lm12;

theorem :: FIELD_15:47
for R being non degenerated unital doubleLoopStr
for n being non zero Nat
for a being Element of R holds LC (X^ (n,a)) = 1. R by Lm13;

theorem teval: :: FIELD_15:48
for R being non degenerated Ring
for n being non zero Nat
for a, x being Element of R holds eval ((X^ (n,a)),x) = (x |^ n) - a
proof end;

theorem split1: :: FIELD_15:49
for F being Field
for n being non zero Nat
for a, b being Element of F holds
( b is_a_root_of X^ (n,a) iff b |^ n = a )
proof end;

theorem split2: :: FIELD_15:50
for F being Field
for E being FieldExtension of F
for n being non zero Nat
for a being Element of F
for b being Element of E st b = a holds
X^ (n,a) = X^ (n,b)
proof end;

theorem :: FIELD_15:51
for R being non degenerated commutative Ring
for n being non trivial Nat
for a being Element of R holds (Deriv R) . (X^ (n,a)) = n * (X^ ((n - 1),(0. R)))
proof end;

theorem :: FIELD_15:52
for p being Prime
for R being commutative b1 -characteristic Ring
for a being Element of R holds (Deriv R) . (X^ (p,a)) = 0_. R
proof end;

theorem split0: :: FIELD_15:53
for p being Prime
for F being b1 -characteristic Field
for a, b being Element of F st b |^ p = a holds
X^ (p,a) = (X- b) |^ p
proof end;

theorem pirred: :: FIELD_15:54
for p being Prime
for F being b1 -characteristic Field
for a being Element of F st ( for b being Element of F holds not b |^ p = a ) holds
X^ (p,a) is irreducible
proof end;

theorem :: FIELD_15:55
for F being Field
for p being non zero Polynomial of F
for a being Element of F holds deg p >= multiplicity (p,a) by ro00;

theorem mulzero1: :: FIELD_15:56
for F being Field
for p being non zero Polynomial of F
for a being Element of F
for n being Element of NAT holds
( (X- a) `^ n divides p iff multiplicity (p,a) >= n )
proof end;

theorem mulzero: :: FIELD_15:57
for F being Field
for E being FieldExtension of F
for p being non zero Element of the carrier of (Polynom-Ring F)
for a being Element of E holds
( a is_a_root_of p,E iff multiplicity (p,a) >= 1 )
proof end;

multi3a: for F being Field
for p being non zero Polynomial of F
for E being FieldExtension of F
for a being Element of F holds multiplicity (p,a) <= multiplicity (p,(@ (a,E)))
proof end;

multi3: for F being Field
for p being non zero Polynomial of F
for E being FieldExtension of F
for a being Element of F holds multiplicity (p,a) = multiplicity (p,(@ (a,E)))
proof end;

multi3K: for F being Field
for p being non zero Polynomial of F
for E being FieldExtension of F
for K being b3 -extending FieldExtension of F
for a being Element of E holds multiplicity (p,a) = multiplicity (p,(@ (a,K)))
proof end;

theorem sepsep: :: FIELD_15:58
for F being Field
for p being non zero Polynomial of F
for E being FieldExtension of F
for q being non zero Polynomial of E st q = p holds
for K being b3 -extending FieldExtension of F
for a being Element of K holds multiplicity (q,a) = multiplicity (p,a)
proof end;

theorem sepsep1: :: FIELD_15:59
for F being Field
for p being non zero Polynomial of F
for E being FieldExtension of F
for q being non zero Polynomial of E st q = p holds
for a being Element of E holds multiplicity (q,a) = multiplicity (p,a)
proof end;

theorem lems: :: FIELD_15:60
for F being Field
for p being non zero Polynomial of F
for c being non zero Element of F
for a being Element of F holds multiplicity ((c * p),a) = multiplicity (p,a)
proof end;

theorem lems1: :: FIELD_15:61
for F being Field
for E being FieldExtension of F
for p being non zero Polynomial of F
for c being non zero Element of F
for a being Element of E holds multiplicity ((c * p),a) = multiplicity (p,a)
proof end;

theorem UP55: :: FIELD_15:62
for F being Field
for E being FieldExtension of F
for p, q being non zero Polynomial of F
for a being Element of E holds multiplicity ((p *' q),a) = (multiplicity (p,a)) + (multiplicity (q,a))
proof end;

theorem multiiso: :: FIELD_15:63
for F being Field
for p being non zero Polynomial of F
for E1, E2 being FieldExtension of F
for i being Function of E1,E2 st i is F -fixing & i is isomorphism holds
for a being Element of E1 holds multiplicity (p,a) = multiplicity (p,(i . a))
proof end;

theorem :: FIELD_15:64
for F being Field
for p being non zero Polynomial of F
for E being FieldExtension of F
for a being Element of F holds multiplicity (p,(@ (a,E))) = multiplicity (p,a) by multi3;

theorem :: FIELD_15:65
for F being Field
for p being non zero Polynomial of F
for E being FieldExtension of F
for K being b3 -extending FieldExtension of F
for a being Element of E holds multiplicity (p,(@ (a,K))) = multiplicity (p,a) by multi3K;

theorem multi4b: :: FIELD_15:66
for F being Field
for p being non zero Polynomial of F
for q being Polynomial of F
for a being Element of F st p = ((X- a) `^ (multiplicity (p,a))) *' q holds
eval (q,a) <> 0. F
proof end;

ABC1: for F being Field
for p being non zero Polynomial of F st ex a being Element of F st multiplicity (p,a) > 1 holds
card (Roots p) < card (BRoots p)
proof end;

theorem ABC: :: FIELD_15:67
for F being Field
for p being non zero Polynomial of F holds
( card (Roots p) < card (BRoots p) iff ex a being Element of F st multiplicity (p,a) > 1 )
proof end;

theorem ThsepsplB: :: FIELD_15:68
for F being Field
for p being non zero Polynomial of F
for a being Element of F holds multiplicity ((NormPolynomial p),a) = multiplicity (p,a)
proof end;

theorem ThsepsplA: :: FIELD_15:69
for F being Field
for p being non constant Polynomial of F holds
( deg p = card (Roots p) iff ( p splits_in F & ( for a being Element of F holds multiplicity (p,a) <= 1 ) ) )
proof end;

multi4d: for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for a being Element of F
for n being Element of NAT
for q being Polynomial of F st q = n * p & eval (p,a) = 0. F holds
eval (q,a) = 0. F
proof end;

theorem multi4: :: FIELD_15:70
for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F)
for a being Element of F st a is_a_root_of p holds
( ( multiplicity (p,a) = 1 implies eval (((Deriv F) . p),a) <> 0. F ) & ( eval (((Deriv F) . p),a) <> 0. F implies multiplicity (p,a) = 1 ) & ( multiplicity (p,a) > 1 implies eval (((Deriv F) . p),a) = 0. F ) & ( eval (((Deriv F) . p),a) = 0. F implies multiplicity (p,a) > 1 ) )
proof end;

mm0: for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring F) st p gcd q <> 1_. F holds
deg (p gcd q) > 0
proof end;

mm1: for F being Field
for p, q being Polynomial of F
for a being Element of F st q divides p & a is_a_root_of q holds
a is_a_root_of p
proof end;

theorem :: FIELD_15:71
for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F) holds
( ex a being Element of F st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) is with_roots )
proof end;

theorem lemsep3: :: FIELD_15:72
for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F st p splits_in E holds
( ex a being Element of E st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) <> 1_. F )
proof end;

theorem lemsep1: :: FIELD_15:73
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F st p splits_in E holds
( ex a being Element of E st multiplicity (p,a) > 1 iff (Deriv F) . p = 0_. F )
proof end;

theorem DP0: :: FIELD_15:74
for p being Prime
for R being commutative b1 -characteristic Ring
for f being Element of the carrier of (Polynom-Ring R) holds
( (Deriv R) . f = 0_. R iff for i being Nat st i in Support f holds
p divides i )
proof end;

definition
let F be Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
attr p is separable means :: FIELD_15:def 3
 for a being Element of the SplittingField of p st a is_a_root_of p, the SplittingField of p holds
multiplicity (p,a) = 1;
end;

:: deftheorem defines separable FIELD_15:def 3 :
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for a being Element of the SplittingField of p st a is_a_root_of p, the SplittingField of p holds
multiplicity (p,a) = 1 );

notation
let F be Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
antonym inseparable p for separable ;
end;

ThSep01: for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 )
proof end;

registration
let F be Field;
cluster Relation-like NAT -defined the carrier of F -valued Function-like quasi_total non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support non zero monic non constant factorizable uniquely_factorizable non unital separable for Element of the carrier of (Polynom-Ring F);
existence
ex b1 being monic non constant Element of the carrier of (Polynom-Ring F) st b1 is separable
proof end;
cluster Relation-like NAT -defined the carrier of F -valued Function-like quasi_total non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support non zero monic non constant factorizable uniquely_factorizable non unital inseparable for Element of the carrier of (Polynom-Ring F);
existence
ex b1 being monic non constant Element of the carrier of (Polynom-Ring F) st b1 is inseparable
proof end;
end;

theorem ThSep0: :: FIELD_15:75
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being FieldExtension of F st p splits_in E holds
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 )
proof end;

theorem ThSep1: :: FIELD_15:76
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) )
proof end;

theorem ThSep02: :: FIELD_15:77
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being FieldExtension of F
for a being Element of E holds multiplicity (p,a) <= 1 )
proof end;

theorem ThSep03: :: FIELD_15:78
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff ex E being FieldExtension of F st
( p splits_in E & ( for a being Element of E holds multiplicity (p,a) <= 1 ) ) )
proof end;

theorem Thsepspl: :: FIELD_15:79
for F being Field
for p being non constant separable Element of the carrier of (Polynom-Ring F) holds
( deg p = card (Roots p) iff p splits_in F )
proof end;

theorem Thsepgcd: :: FIELD_15:80
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff p gcd ((Deriv F) . p) = 1_. F )
proof end;

theorem main1: :: FIELD_15:81
for F being Field
for p being non constant irreducible Element of the carrier of (Polynom-Ring F) holds
( p is separable iff (Deriv F) . p <> 0_. F )
proof end;

theorem lempp: :: FIELD_15:82
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being SplittingField of p ex a being Element of E ex q being Ppoly of E,(Roots (E,p)) st p = a * q )
proof end;

theorem :: FIELD_15:83
for F being Field
for p being monic non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being SplittingField of p holds p is Ppoly of E,(Roots (E,p)) )
proof end;

theorem :: FIELD_15:84
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being FieldExtension of F st p splits_in E holds
p is_square-free_over E )
proof end;

theorem :: FIELD_15:85
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff ex E being FieldExtension of F st card (Roots (E,p)) = deg p )
proof end;

theorem :: FIELD_15:86
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for a being non zero Element of F holds
( a * p is separable iff p is separable )
proof end;

theorem ThSepPR: :: FIELD_15:87
for F being Field
for p, q being non constant Element of the carrier of (Polynom-Ring F)
for r being Element of the carrier of (Polynom-Ring F) st p = q *' r & p is separable holds
q is separable
proof end;

theorem YY: :: FIELD_15:88
for F being Field
for E being FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F)
for q being non constant Element of the carrier of (Polynom-Ring E) st p = q holds
( p is separable iff q is separable )
proof end;

registration
let F be Field;
let a be Element of F;
cluster X- a -> irreducible separable ;
coherence
( X- a is separable & X- a is irreducible )
proof end;
end;

registration
let F be Field;
let a be Element of F;
let n be non trivial Nat;
cluster (X- a) |^ n -> reducible inseparable ;
coherence
( not (X- a) |^ n is separable & not (X- a) |^ n is irreducible )
proof end;
end;

registration
let F be 0 -characteristic Field;
cluster irreducible -> irreducible separable for Element of the carrier of (Polynom-Ring F);
coherence
for b1 being irreducible Element of the carrier of (Polynom-Ring F) holds b1 is separable
proof end;
end;

theorem contr: :: FIELD_15:89
for p being Prime
for F being b1 -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 )
proof end;

definition
let F be Field;
attr F is perfect means :dpf: :: FIELD_15:def 4
 for p being irreducible Element of the carrier of (Polynom-Ring F) holds p is separable ;
end;

:: deftheorem dpf defines perfect FIELD_15:def 4 :
for F being Field holds
( F is perfect iff for p being irreducible Element of the carrier of (Polynom-Ring F) holds p is separable );

registration
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative 0 -characteristic -> 0 -characteristic perfect for doubleLoopStr ;
coherence
for b1 being 0 -characteristic Field holds b1 is perfect ;
end;

theorem DP1: :: FIELD_15:90
for p being Prime
for F being b1 -characteristic Field
for q being Element of the carrier of (Polynom-Ring F) st ( for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i ) ) holds
ex r being Element of the carrier of (Polynom-Ring F) st r |^ p = q
proof end;

theorem Fpp: :: FIELD_15:91
for p being Prime
for F being b1 -characteristic Field holds
( F is perfect iff F == F |^ p )
proof end;

theorem CF: :: FIELD_15:92
for F being Field holds
( F is finite iff ex n being non zero Nat st card F = (Char F) |^ n )
proof end;

theorem Fpp1: :: FIELD_15:93
for p being Prime
for F being finite b1 -characteristic Field
for a being Element of F ex b being Element of F st b |^ p = a
proof end;

registration
cluster non empty non degenerated finite right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative -> finite perfect for doubleLoopStr ;
coherence
for b1 being finite Field holds b1 is perfect
proof end;
end;

registration
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative algebraic-closed -> algebraic-closed perfect for doubleLoopStr ;
coherence
for b1 being algebraic-closed Field holds b1 is perfect
proof end;
end;

definition
let F be Field;
let E be FieldExtension of F;
let a be Element of E;
attr a is F -separable means :defsep: :: FIELD_15:def 5
 ex b being F -algebraic Element of E st
( b = a & MinPoly (b,F) is separable );
end;

:: deftheorem defsep defines -separable FIELD_15:def 5 :
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -separable iff ex b being b1 -algebraic Element of E st
( b = a & MinPoly (b,F) is separable ) );

registration
let F be Field;
let E be FieldExtension of F;
cluster non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable non irreducible F -separable for Element of the carrier of E;
existence
ex b1 being Element of E st
( not b1 is zero & b1 is F -separable )
proof end;
end;

registration
let F be Field;
let E be FieldExtension of F;
cluster F -separable -> F -algebraic for Element of the carrier of E;
coherence
for b1 being Element of E st b1 is F -separable holds
b1 is F -algebraic ;
end;

registration
let F be Field;
let E be FieldExtension of F;
let a be F -separable Element of E;
cluster minimal_polynom (a,F) -> separable ;
coherence
MinPoly (a,F) is separable
proof end;
end;

definition
let F be Field;
let E be FieldExtension of F;
attr E is F -separable means :defsepF: :: FIELD_15:def 6
( E is F -algebraic & ( for a being Element of E holds a is F -separable ) );
end;

:: deftheorem defsepF defines -separable FIELD_15:def 6 :
for F being Field
for E being FieldExtension of F holds
( E is F -separable iff ( E is F -algebraic & ( for a being Element of E holds a is F -separable ) ) );

notation
let F be Field;
let E be FieldExtension of F;
antonym F -inseparable E for F -separable ;
end;

registration
let F be Field;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID F -homomorphic factorial F -monomorphic F -extending F -finite F -separable for doubleLoopStr ;
existence
ex b1 being FieldExtension of F st
( b1 is F -finite & b1 is F -separable )
proof end;
end;

registration
let F be Field;
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative F -extending F -separable -> F -algebraic for doubleLoopStr ;
coherence
for b1 being FieldExtension of F st b1 is F -separable holds
b1 is F -algebraic ;
end;

registration
let F be Field;
let E be F -separable FieldExtension of F;
cluster -> F -separable for Element of the carrier of E;
coherence
for b1 being Element of E holds b1 is F -separable by defsepF;
end;

theorem :: FIELD_15:94
for F being Field
for K being FieldExtension of F
for E being b2 -extending FieldExtension of F st E is F -separable holds
( E is K -separable & K is F -separable )
proof end;

registration
let F be perfect Field;
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative F -extending F -algebraic -> F -algebraic F -separable for doubleLoopStr ;
coherence
for b1 being F -algebraic FieldExtension of F holds b1 is F -separable
proof end;
end;

registration
let F be perfect Field;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like PID F -homomorphic factorial F -monomorphic F -extending F -normal F -separable for doubleLoopStr ;
existence
ex b1 being FieldExtension of F st
( b1 is F -normal & b1 is F -separable )
proof end;
end;

registration
let F be perfect Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
cluster -> F -normal F -separable for SplittingField of p;
coherence
for b1 being SplittingField of p holds
( b1 is F -normal & b1 is F -separable ) ;
end;