:: by Christoph Schwarzweller

::

:: Received March 28, 2019

:: Copyright (c) 2019 Association of Mizar Users

notation
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 )

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

end;
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;

registration

let R be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

let f be additive Function of R,R;

reducibility

f . (0. R) = 0. R by RING_2:6;

end;
let f be additive Function of R,R;

reducibility

f . (0. R) = 0. R by RING_2:6;

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))

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;

:: 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 ) );

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

ex b_{1} being domRing st

( not b_{1} is almost_left_invertible & b_{1} is factorial )
;

end;

cluster non empty non degenerated V62() left_add-cancelable right_add-cancelable left_complementable right_complementable almost_left_cancelable almost_right_cancelable non almost_left_invertible right-distributive left-distributive right_unital well-unital V111() left_unital Abelian add-associative right_zeroed V128() unital V133() V135() domRing-like V250() V251() V252() V253() K717() -homomorphic factorial for doubleLoopStr ;

existence ex b

( not b

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

for a being non zero NonUnit of R ex b being Element of R st b is_a_irreducible_factor_of a

proof 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;

coherence

not anpoly (a,n) is zero

end;
let a be non zero Element of R;

let n be Nat;

coherence

not anpoly (a,n) is zero

proof end;

registration
end;

theorem :: FIELD_1:4

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

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)

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

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))

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)

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))

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))

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)

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 b_{1} -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

for S being b

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 b_{1} -homomorphic Ring

for h being Homomorphism of R,S holds h . (Sum (<*> the carrier of R)) = 0. S

for S being b

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 b_{1} -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))

for S being b

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 b_{1} -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)

for S being b

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 b_{1} -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))

for S being b

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 b_{1} -homomorphic Ring

for h being Homomorphism of R,S holds h . (Product (<*> the carrier of R)) = 1. S

for S being b

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 b_{1} -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 . (Product F))

for S being b

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 . (Product F))

proof end;

theorem :: FIELD_1:20

for R being Ring

for S being b_{1} -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 . (Product F)) * (h . a)

for S being b

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 . (Product F)) * (h . a)

proof end;

theorem :: FIELD_1:21

for R being Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S

for F, G being FinSequence of R holds h . (Product (F ^ G)) = (h . (Product F)) * (h . (Product G))

for S being b

for h being Homomorphism of R,S

for F, G being FinSequence of R holds h . (Product (F ^ G)) = (h . (Product F)) * (h . (Product G))

proof end;

definition

let R, S be Ring;

let f be Function of (Polynom-Ring R),(Polynom-Ring S);

let p be Element of the carrier of (Polynom-Ring R);

:: original: .

redefine func f . p -> Element of the carrier of (Polynom-Ring S);

coherence

f . p is Element of the carrier of (Polynom-Ring S)

end;
let f be Function of (Polynom-Ring R),(Polynom-Ring S);

let p be Element of the carrier of (Polynom-Ring R);

:: original: .

redefine func f . p -> Element of the carrier of (Polynom-Ring S);

coherence

f . p is Element of the carrier of (Polynom-Ring S)

proof end;

definition

let R be Ring;

let S be R -homomorphic Ring;

let h be additive Function of R,S;

ex b_{1} being Function of (Polynom-Ring R),(Polynom-Ring S) st

for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b_{1} . f) . i = h . (f . i)

for b_{1}, b_{2} being Function of (Polynom-Ring R),(Polynom-Ring S) st ( for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b_{1} . f) . i = h . (f . i) ) & ( for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b_{2} . f) . i = h . (f . i) ) holds

b_{1} = b_{2}

end;
let S be R -homomorphic Ring;

let h be additive Function of R,S;

func PolyHom h -> Function of (Polynom-Ring R),(Polynom-Ring S) means :Def2: :: FIELD_1:def 2

for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (it . f) . i = h . (f . i);

existence for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (it . f) . i = h . (f . i);

ex b

for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b

proof end;

uniqueness for b

for i being Nat holds (b

for i being Nat holds (b

b

proof end;

:: deftheorem Def2 defines PolyHom FIELD_1:def 2 :

for R being Ring

for S being b_{1} -homomorphic Ring

for h being additive Function of R,S

for b_{4} being Function of (Polynom-Ring R),(Polynom-Ring S) holds

( b_{4} = PolyHom h iff for f being Element of the carrier of (Polynom-Ring R)

for i being Nat holds (b_{4} . f) . i = h . (f . i) );

for R being Ring

for S being b

for h being additive Function of R,S

for b

( b

for i being Nat holds (b

registration

let R be Ring;

let S be R -homomorphic Ring;

let h be Homomorphism of R,S;

coherence

( PolyHom h is additive & PolyHom h is multiplicative & PolyHom h is unity-preserving )

end;
let S be R -homomorphic Ring;

let h be Homomorphism of R,S;

coherence

( PolyHom h is additive & PolyHom h is multiplicative & PolyHom h is unity-preserving )

proof end;

theorem Th23: :: FIELD_1:22

for R being Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S holds (PolyHom h) . (0_. R) = 0_. S

for S being b

for h being Homomorphism of R,S holds (PolyHom h) . (0_. R) = 0_. S

proof end;

theorem :: FIELD_1:23

for R being Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S holds (PolyHom h) . (1_. R) = 1_. S

for S being b

for h being Homomorphism of R,S holds (PolyHom h) . (1_. R) = 1_. S

proof end;

theorem :: FIELD_1:24

for R being Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S

for p, q being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (p + q) = ((PolyHom h) . p) + ((PolyHom h) . q) by VECTSP_1:def 20;

for S being b

for h being Homomorphism of R,S

for p, q being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (p + q) = ((PolyHom h) . p) + ((PolyHom h) . q) by VECTSP_1:def 20;

theorem :: FIELD_1:25

for R being Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S

for p, q being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (p * q) = ((PolyHom h) . p) * ((PolyHom h) . q) by GROUP_6:def 6;

for S being b

for h being Homomorphism of R,S

for p, q being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (p * q) = ((PolyHom h) . p) * ((PolyHom h) . q) by GROUP_6:def 6;

theorem Th27: :: FIELD_1:26

for R being Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for b being Element of R holds (PolyHom h) . (b * p) = (h . b) * ((PolyHom h) . p)

for S being b

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for b being Element of R holds (PolyHom h) . (b * p) = (h . b) * ((PolyHom h) . p)

proof end;

Lm2: for R being Ring

for S being b

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds len ((PolyHom h) . p) <= len p

proof end;

Lm3: for R being Ring

for S being b

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) st len p <> 0 holds

( len ((PolyHom h) . p) = len p iff h . (p . ((len p) -' 1)) <> 0. S )

proof end;

Lm4: for R being Ring

for S being b

for h being Homomorphism of R,S

for p, L being Element of the carrier of (Polynom-Ring R) st L = LM p holds

for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))

proof end;

theorem Th28: :: FIELD_1:27

for R being Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for a being Element of R holds h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))

for S being b

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for a being Element of R holds h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))

proof end;

:: RING_5:7 is required domRing

theorem :: FIELD_1:28

for R being domRing

for S being b_{1} -homomorphic domRing

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for b, x being Element of R holds h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))

for S being b

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for b, x being Element of R holds h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))

proof end;

registration

let R be Ring;

ex b_{1} being Ring st

( b_{1} is R -homomorphic & b_{1} is R -monomorphic )

ex b_{1} being Ring st

( b_{1} is R -homomorphic & b_{1} is R -isomorphic )

end;
cluster non empty left_add-cancelable right_add-cancelable left_complementable right_complementable right-distributive left-distributive right_unital well-unital V111() left_unital Abelian add-associative right_zeroed V128() unital V133() V250() V251() V252() V253() R -homomorphic K717() -homomorphic K717() -homomorphic R -monomorphic for doubleLoopStr ;

existence ex b

( b

proof end;

cluster non empty left_add-cancelable right_add-cancelable left_complementable right_complementable right-distributive left-distributive right_unital well-unital V111() left_unital Abelian add-associative right_zeroed V128() unital V133() V250() V251() V252() V253() R -homomorphic K717() -homomorphic K717() -homomorphic R -isomorphic for doubleLoopStr ;

existence ex b

( b

proof end;

registration

let R be Ring;

for b_{1} being Ring st b_{1} is R -monomorphic holds

b_{1} is R -homomorphic
;

end;
cluster non empty right_complementable well-unital V111() Abelian add-associative right_zeroed V133() R -monomorphic -> R -homomorphic for doubleLoopStr ;

coherence for b

b

registration

let R be Ring;

let S be R -homomorphic R -monomorphic Ring;

let h be Monomorphism of R,S;

coherence

PolyHom h is RingMonomorphism

end;
let S be R -homomorphic R -monomorphic Ring;

let h be Monomorphism of R,S;

coherence

PolyHom h is RingMonomorphism

proof end;

registration

let R be Ring;

let S be R -homomorphic R -isomorphic Ring;

let h be Isomorphism of R,S;

coherence

PolyHom h is RingIsomorphism

end;
let S be R -homomorphic R -isomorphic Ring;

let h be Isomorphism of R,S;

coherence

PolyHom h is RingIsomorphism

proof end;

theorem :: FIELD_1:29

for R being Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) <= deg p by Lm2, XREAL_1:6;

for S being b

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) <= deg p by Lm2, XREAL_1:6;

theorem :: FIELD_1:30

for R being non degenerated Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S

for p being non zero Element of the carrier of (Polynom-Ring R) holds

( deg ((PolyHom h) . p) = deg p iff h . (LC p) <> 0. S )

for S being b

for h being Homomorphism of R,S

for p being non zero Element of the carrier of (Polynom-Ring R) holds

( deg ((PolyHom h) . p) = deg p iff h . (LC p) <> 0. S )

proof end;

theorem Th32: :: FIELD_1:31

for R being Ring

for S being b_{1} -homomorphic b_{1} -monomorphic Ring

for h being Monomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) = deg p

for S being b

for h being Monomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) = deg p

proof end;

theorem Th33: :: FIELD_1:32

for R being Ring

for S being b_{1} -homomorphic b_{1} -monomorphic Ring

for h being Monomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds LM ((PolyHom h) . p) = (PolyHom h) . (LM p)

for S being b

for h being Monomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds LM ((PolyHom h) . p) = (PolyHom h) . (LM p)

proof end;

theorem Th34: :: FIELD_1:33

for R being Ring

for S being b_{1} -homomorphic Ring

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for a being Element of R st a is_a_root_of p holds

h . a is_a_root_of (PolyHom h) . p

for S being b

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for a being Element of R st a is_a_root_of p holds

h . a is_a_root_of (PolyHom h) . p

proof end;

theorem Th35: :: FIELD_1:34

for R being Ring

for S being b_{1} -homomorphic b_{1} -monomorphic Ring

for h being Monomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for a being Element of R holds

( a is_a_root_of p iff h . a is_a_root_of (PolyHom h) . p )

for S being b

for h being Monomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for a being Element of R holds

( a is_a_root_of p iff h . a is_a_root_of (PolyHom h) . p )

proof end;

theorem Th36: :: FIELD_1:35

for R being Ring

for S being b_{1} -homomorphic b_{1} -isomorphic Ring

for h being Isomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for b being Element of S holds

( b is_a_root_of (PolyHom h) . p iff ex a being Element of R st

( a is_a_root_of p & h . a = b ) )

for S being b

for h being Isomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R)

for b being Element of S holds

( b is_a_root_of (PolyHom h) . 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 b_{1} -homomorphic Ring

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds Roots p c= { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }

for S being b

for h being Homomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds Roots p c= { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }

proof end;

theorem :: FIELD_1:37

for R being Ring

for S being b_{1} -homomorphic b_{1} -monomorphic Ring

for h being Monomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds Roots p = { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }

for S being b

for h being Monomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds Roots p = { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }

proof end;

theorem Th39: :: FIELD_1:38

for R being Ring

for S being b_{1} -homomorphic b_{1} -isomorphic Ring

for h being Isomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds Roots ((PolyHom h) . p) = { (h . a) where a is Element of R : a in Roots p }

for S being b

for h being Isomorphism of R,S

for p being Element of the carrier of (Polynom-Ring R) holds Roots ((PolyHom h) . 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 (Polynom-Ring F);

coherence

(Polynom-Ring F) / ({p} -Ideal) is Field ;

end;
let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

(Polynom-Ring F) / ({p} -Ideal) is Field ;

:: deftheorem defines KroneckerField FIELD_1:def 3 :

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds KroneckerField (F,p) = (Polynom-Ring F) / ({p} -Ideal);

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds KroneckerField (F,p) = (Polynom-Ring F) / ({p} -Ideal);

definition

let F be Field;

let p be irreducible Element of the carrier of (Polynom-Ring F);

(canHom ({p} -Ideal)) * (canHom F) is Function of F,(KroneckerField (F,p)) ;

end;
let p be irreducible Element of the carrier of (Polynom-Ring F);

func emb p -> Function of F,(KroneckerField (F,p)) equals :: FIELD_1:def 4

(canHom ({p} -Ideal)) * (canHom F);

coherence (canHom ({p} -Ideal)) * (canHom F);

(canHom ({p} -Ideal)) * (canHom F) is Function of F,(KroneckerField (F,p)) ;

:: deftheorem defines emb FIELD_1:def 4 :

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds emb p = (canHom ({p} -Ideal)) * (canHom F);

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds emb p = (canHom ({p} -Ideal)) * (canHom F);

registration

let F be Field;

let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

( emb p is additive & emb p is multiplicative & emb p is unity-preserving ) ;

end;
let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

( emb p is additive & emb p is multiplicative & emb p is unity-preserving ) ;

registration

let F be Field;

let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

emb p is RingMonomorphism ;

end;
let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

emb p is RingMonomorphism ;

registration

let F be Field;

let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

( KroneckerField (F,p) is F -homomorphic & KroneckerField (F,p) is F -monomorphic )

end;
let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

( KroneckerField (F,p) is F -homomorphic & KroneckerField (F,p) is F -monomorphic )

proof end;

definition

let F be Field;

let p be irreducible Element of the carrier of (Polynom-Ring F);

let f be Element of the carrier of (Polynom-Ring F);

(PolyHom (emb p)) . f is Element of the carrier of (Polynom-Ring (KroneckerField (F,p))) ;

end;
let p be irreducible Element of the carrier of (Polynom-Ring F);

let f be Element of the carrier of (Polynom-Ring F);

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;

(PolyHom (emb p)) . f is Element of the carrier of (Polynom-Ring (KroneckerField (F,p))) ;

:: deftheorem defines emb FIELD_1:def 5 :

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F)

for f being Element of the carrier of (Polynom-Ring F) holds emb (f,p) = (PolyHom (emb p)) . f;

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F)

for f being Element of the carrier of (Polynom-Ring F) holds emb (f,p) = (PolyHom (emb p)) . f;

definition

let F be Field;

let p be irreducible Element of the carrier of (Polynom-Ring F);

Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>) is Element of (KroneckerField (F,p))

end;
let p be irreducible Element of the carrier of (Polynom-Ring F);

func KrRoot p -> Element of (KroneckerField (F,p)) equals :: FIELD_1:def 6

Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>);

coherence Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>);

Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>) is Element of (KroneckerField (F,p))

proof end;

:: deftheorem defines KrRoot FIELD_1:def 6 :

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRoot p = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>);

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRoot p = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>);

theorem Th40: :: FIELD_1:39

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F)

for a being Element of F holds (emb p) . a = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(a | F))

for p being irreducible Element of the carrier of (Polynom-Ring F)

for a being Element of F holds (emb p) . a = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(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 (Polynom-Ring F)

for f being Element of the carrier of (Polynom-Ring F) holds (emb (f,p)) . n = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((f . n) | F))

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F)

for f being Element of the carrier of (Polynom-Ring F) holds (emb (f,p)) . n = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((f . n) | F))

proof end;

Lm5: for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F)

for f being Element of the carrier of (Polynom-Ring F) holds eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))

proof end;

theorem Th42: :: FIELD_1:41

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F)

for f being Element of the carrier of (Polynom-Ring F) holds eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)

for p being irreducible Element of the carrier of (Polynom-Ring F)

for f being Element of the carrier of (Polynom-Ring F) holds eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)

proof end;

theorem Th43: :: FIELD_1:42

for F being Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRoot p is_a_root_of emb (p,p)

for p being irreducible Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) st not f is constant holds

ex p being irreducible Element of the carrier of (Polynom-Ring F) st emb (f,p) is with_roots

for f being Element of the carrier of (Polynom-Ring F) st not f is constant holds

ex p being irreducible Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) st emb p is isomorphism holds

p is with_roots

for p being irreducible Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) st not p is with_roots holds

not emb p is isomorphism by Th45;

for p being irreducible Element of the carrier of (Polynom-Ring F) st not p is with_roots holds

not emb p is isomorphism by Th45;