:: On Roots of Polynomials over K[X]/<p>
:: by Christoph Schwarzweller
::
:: Copyright (c) 2019-2021 Association of Mizar Users

notation
let L be non empty ZeroStr ;
let p be Polynomial of L;
synonym LM p for Leading-Monomial p;
end;

theorem Th2: :: FIELD_1:1
for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )
proof end;

definition
let R be non degenerated Ring;
let p be non zero Polynomial of R;
:: original: deg
redefine func deg p -> Element of NAT ;
coherence
deg p is Element of NAT
proof end;
end;

registration
let R be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;
let f be additive Function of R,R;
reduce f . (0. R) to 0. R;
reducibility
f . (0. R) = 0. R
by RING_2:6;
end;

theorem Th3: :: FIELD_1:2
for R being Ring
for I being Ideal of R
for x being Element of (R / I)
for a being Element of R st x = Class ((EqRel (R,I)),a) holds
for n being Nat holds x |^ n = Class ((EqRel (R,I)),(a |^ n))
proof end;

definition
let R be Ring;
let a, b be Element of R;
pred b is_a_irreducible_factor_of a means :: FIELD_1:def 1
( b divides a & b is irreducible );
end;

:: deftheorem defines is_a_irreducible_factor_of FIELD_1:def 1 :
for R being Ring
for a, b being Element of R holds
( b is_a_irreducible_factor_of a iff ( b divides a & b is irreducible ) );

registration
existence
ex b1 being domRing st
( not b1 is almost_left_invertible & b1 is factorial )
;
end;

theorem Th4: :: FIELD_1:3
for R being non almost_left_invertible factorial domRing
for a being non zero NonUnit of R ex b being Element of R st b is_a_irreducible_factor_of a
proof end;

notation
let R be Ring;
let a be Element of R;
let n be Nat;
synonym anpoly (a,n) for seq (n,a);
end;

Lm1: for n being Nat
for R being non degenerated Ring
for a being non zero Element of R holds deg (anpoly (a,n)) = n

proof end;

registration
let R be non degenerated Ring;
let a be non zero Element of R;
let n be Nat;
cluster anpoly (a,n) -> non zero ;
coherence
not anpoly (a,n) is zero
proof end;
end;

registration
let R be Ring;
let a be zero Element of R;
let n be Nat;
cluster anpoly (a,n) -> zero ;
coherence
anpoly (a,n) is zero
proof end;
end;

theorem :: FIELD_1:4
for n being Nat
for R being non degenerated Ring
for a being non zero Element of R holds deg (anpoly (a,n)) = n by Lm1;

theorem :: FIELD_1:5
for n being Nat
for R being non degenerated Ring
for a being Element of R holds LC (anpoly (a,n)) = a
proof end;

theorem :: FIELD_1:6
for R being non degenerated Ring
for n being non zero Nat
for a, x being Element of R holds eval ((anpoly (a,n)),x) = a * (x |^ n)
proof end;

theorem :: FIELD_1:7
for R being non degenerated Ring
for a being Element of R holds anpoly (a,0) = a | R ;

theorem Th9: :: FIELD_1:8
for R being non degenerated Ring
for n being non zero Element of NAT holds anpoly ((1. R),n) = rpoly (n,(0. R))
proof end;

theorem Th10: :: FIELD_1:9
for n being Nat
for R being non degenerated comRing
for a, b being non zero Element of R holds b * (anpoly (a,n)) = anpoly ((a * b),n)
proof end;

theorem Th11: :: FIELD_1:10
for R being non degenerated comRing
for a, b being non zero Element of R
for n, m being Nat holds (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m))
proof end;

theorem Th12: :: FIELD_1:11
for R being non degenerated Ring
for p being non zero Polynomial of R holds LM p = anpoly ((p . (deg p)),(deg p))
proof end;

theorem Th13: :: FIELD_1:12
for n being Nat
for R being non degenerated comRing holds <%(0. R),(1. R)%> `^ n = anpoly ((1. R),n)
proof end;

theorem Th14: :: FIELD_1:13
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R
for n being Nat holds h . (a |^ n) = (h . a) |^ n
proof end;

theorem :: FIELD_1:14
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S holds h . (Sum (<*> the carrier of R)) = 0. S
proof end;

theorem :: FIELD_1:15
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F being FinSequence of R
for a being Element of R holds h . (Sum (<*a*> ^ F)) = (h . a) + (h . (Sum F))
proof end;

theorem Th17: :: FIELD_1:16
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F being FinSequence of R
for a being Element of R holds h . (Sum (F ^ <*a*>)) = (h . (Sum F)) + (h . a)
proof end;

theorem :: FIELD_1:17
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F, G being FinSequence of R holds h . (Sum (F ^ G)) = (h . (Sum F)) + (h . (Sum G))
proof end;

theorem :: FIELD_1:18
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S holds h . (Product (<*> the carrier of R)) = 1. S
proof end;

theorem :: FIELD_1:19
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F being FinSequence of R
for a being Element of R holds h . (Product (<*a*> ^ F)) = (h . a) * (h . ())
proof end;

theorem :: FIELD_1:20
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F being FinSequence of R
for a being Element of R holds h . (Product (F ^ <*a*>)) = (h . ()) * (h . a)
proof end;

theorem :: FIELD_1:21
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F, G being FinSequence of R holds h . (Product (F ^ G)) = (h . ()) * (h . ())
proof end;

definition
let R, S be Ring;
let f be Function of (),();
let p be Element of the carrier of ();
:: original: .
redefine func f . p -> Element of the carrier of ();
coherence
f . p is Element of the carrier of ()
proof end;
end;

definition
let R be Ring;
let S be R -homomorphic Ring;
let h be additive Function of R,S;
func PolyHom h -> Function of (),() means :Def2: :: FIELD_1:def 2
for f being Element of the carrier of ()
for i being Nat holds (it . f) . i = h . (f . i);
existence
ex b1 being Function of (),() st
for f being Element of the carrier of ()
for i being Nat holds (b1 . f) . i = h . (f . i)
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for f being Element of the carrier of ()
for i being Nat holds (b1 . f) . i = h . (f . i) ) & ( for f being Element of the carrier of ()
for i being Nat holds (b2 . f) . i = h . (f . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines PolyHom FIELD_1:def 2 :
for R being Ring
for S being b1 -homomorphic Ring
for h being additive Function of R,S
for b4 being Function of (),() holds
( b4 = PolyHom h iff for f being Element of the carrier of ()
for i being Nat holds (b4 . f) . i = h . (f . i) );

registration
let R be Ring;
let S be R -homomorphic Ring;
let h be Homomorphism of R,S;
coherence
proof end;
end;

theorem Th23: :: FIELD_1:22
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S holds () . (0_. R) = 0_. S
proof end;

theorem :: FIELD_1:23
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S holds () . (1_. R) = 1_. S
proof end;

theorem :: FIELD_1:24
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p, q being Element of the carrier of () holds () . (p + q) = (() . p) + (() . q) by VECTSP_1:def 20;

theorem :: FIELD_1:25
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p, q being Element of the carrier of () holds () . (p * q) = (() . p) * (() . q) by GROUP_6:def 6;

theorem Th27: :: FIELD_1:26
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of ()
for b being Element of R holds () . (b * p) = (h . b) * (() . p)
proof end;

Lm2: for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of () holds len (() . p) <= len p

proof end;

Lm3: for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of () st len p <> 0 holds
( len (() . p) = len p iff h . (p . ((len p) -' 1)) <> 0. S )

proof end;

Lm4: for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p, L being Element of the carrier of () st L = LM p holds
for a being Element of R holds h . (eval ((LM p),a)) = eval ((() . L),(h . a))

proof end;

theorem Th28: :: FIELD_1:27
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of ()
for a being Element of R holds h . (eval (p,a)) = eval ((() . p),(h . a))
proof end;

:: RING_5:7 is required domRing
theorem :: FIELD_1:28
for R being domRing
for S being b1 -homomorphic domRing
for h being Homomorphism of R,S
for p being Element of the carrier of ()
for b, x being Element of R holds h . (eval ((b * p),x)) = (h . b) * (eval ((() . p),(h . x)))
proof end;

registration
let R be Ring;
existence
ex b1 being Ring st
( b1 is R -homomorphic & b1 is R -monomorphic )
proof end;
existence
ex b1 being Ring st
( b1 is R -homomorphic & b1 is R -isomorphic )
proof end;
end;

registration
let R be Ring;
coherence
for b1 being Ring st b1 is R -monomorphic holds
b1 is R -homomorphic
;
end;

registration
let R be Ring;
let S be R -homomorphic R -monomorphic Ring;
let h be Monomorphism of R,S;
coherence
proof end;
end;

registration
let R be Ring;
let S be R -homomorphic R -isomorphic Ring;
let h be Isomorphism of R,S;
coherence
proof end;
end;

theorem :: FIELD_1:29
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of () holds deg (() . p) <= deg p by ;

theorem :: FIELD_1:30
for R being non degenerated Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being non zero Element of the carrier of () holds
( deg (() . p) = deg p iff h . (LC p) <> 0. S )
proof end;

theorem Th32: :: FIELD_1:31
for R being Ring
for S being b1 -homomorphic b1 -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of () holds deg (() . p) = deg p
proof end;

theorem Th33: :: FIELD_1:32
for R being Ring
for S being b1 -homomorphic b1 -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of () holds LM (() . p) = () . (LM p)
proof end;

theorem Th34: :: FIELD_1:33
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of ()
for a being Element of R st a is_a_root_of p holds
h . a is_a_root_of () . p
proof end;

theorem Th35: :: FIELD_1:34
for R being Ring
for S being b1 -homomorphic b1 -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of ()
for a being Element of R holds
( a is_a_root_of p iff h . a is_a_root_of () . p )
proof end;

theorem Th36: :: FIELD_1:35
for R being Ring
for S being b1 -homomorphic b1 -isomorphic Ring
for h being Isomorphism of R,S
for p being Element of the carrier of ()
for b being Element of S holds
( b is_a_root_of () . p iff ex a being Element of R st
( a is_a_root_of p & h . a = b ) )
proof end;

theorem Th37: :: FIELD_1:36
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of () holds Roots p c= { a where a is Element of R : h . a in Roots (() . p) }
proof end;

theorem :: FIELD_1:37
for R being Ring
for S being b1 -homomorphic b1 -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of () holds Roots p = { a where a is Element of R : h . a in Roots (() . p) }
proof end;

theorem Th39: :: FIELD_1:38
for R being Ring
for S being b1 -homomorphic b1 -isomorphic Ring
for h being Isomorphism of R,S
for p being Element of the carrier of () holds Roots (() . p) = { (h . a) where a is Element of R : a in Roots p }
proof end;

definition
let F be Field;
let p be irreducible Element of the carrier of ();
func KroneckerField (F,p) -> Field equals :: FIELD_1:def 3
() / ();
coherence
() / () is Field
;
end;

:: deftheorem defines KroneckerField FIELD_1:def 3 :
for F being Field
for p being irreducible Element of the carrier of () holds KroneckerField (F,p) = () / ();

definition
let F be Field;
let p be irreducible Element of the carrier of ();
func emb p -> Function of F,(KroneckerField (F,p)) equals :: FIELD_1:def 4
(canHom ()) * ();
coherence
(canHom ()) * () is Function of F,(KroneckerField (F,p))
;
end;

:: deftheorem defines emb FIELD_1:def 4 :
for F being Field
for p being irreducible Element of the carrier of () holds emb p = (canHom ()) * ();

registration
let F be Field;
let p be irreducible Element of the carrier of ();
coherence
( emb p is additive & emb p is multiplicative & emb p is unity-preserving )
;
end;

registration
let F be Field;
let p be irreducible Element of the carrier of ();
coherence ;
end;

registration
let F be Field;
let p be irreducible Element of the carrier of ();
coherence
( KroneckerField (F,p) is F -homomorphic & KroneckerField (F,p) is F -monomorphic )
proof end;
end;

definition
let F be Field;
let p be irreducible Element of the carrier of ();
let f be Element of the carrier of ();
func emb (f,p) -> Element of the carrier of (Polynom-Ring (KroneckerField (F,p))) equals :: FIELD_1:def 5
(PolyHom (emb p)) . f;
coherence
(PolyHom (emb p)) . f is Element of the carrier of (Polynom-Ring (KroneckerField (F,p)))
;
end;

:: deftheorem defines emb FIELD_1:def 5 :
for F being Field
for p being irreducible Element of the carrier of ()
for f being Element of the carrier of () holds emb (f,p) = (PolyHom (emb p)) . f;

definition
let F be Field;
let p be irreducible Element of the carrier of ();
func KrRoot p -> Element of (KroneckerField (F,p)) equals :: FIELD_1:def 6
Class ((EqRel ((),())),<%(0. F),(1. F)%>);
coherence
Class ((EqRel ((),())),<%(0. F),(1. F)%>) is Element of (KroneckerField (F,p))
proof end;
end;

:: deftheorem defines KrRoot FIELD_1:def 6 :
for F being Field
for p being irreducible Element of the carrier of () holds KrRoot p = Class ((EqRel ((),())),<%(0. F),(1. F)%>);

theorem Th40: :: FIELD_1:39
for F being Field
for p being irreducible Element of the carrier of ()
for a being Element of F holds (emb p) . a = Class ((EqRel ((),())),(a | F))
proof end;

theorem Th41: :: FIELD_1:40
for n being Nat
for F being Field
for p being irreducible Element of the carrier of ()
for f being Element of the carrier of () holds (emb (f,p)) . n = Class ((EqRel ((),())),((f . n) | F))
proof end;

Lm5: for F being Field
for p being irreducible Element of the carrier of ()
for f being Element of the carrier of () holds eval ((LM (emb (f,p))),()) = Class ((EqRel ((),())),(LM f))

proof end;

theorem Th42: :: FIELD_1:41
for F being Field
for p being irreducible Element of the carrier of ()
for f being Element of the carrier of () holds eval ((emb (f,p)),()) = Class ((EqRel ((),())),f)
proof end;

theorem Th43: :: FIELD_1:42
for F being Field
for p being irreducible Element of the carrier of () holds KrRoot p is_a_root_of emb (p,p)
proof end;

theorem :: FIELD_1:43
for F being Field
for f being Element of the carrier of () st not f is constant holds
ex p being irreducible Element of the carrier of () st emb (f,p) is with_roots
proof end;

theorem Th45: :: FIELD_1:44
for F being Field
for p being irreducible Element of the carrier of () st emb p is isomorphism holds
p is with_roots
proof end;

theorem :: FIELD_1:45
for F being Field
for p being irreducible Element of the carrier of () st not p is with_roots holds
not emb p is isomorphism by Th45;