:: by Christoph Schwarzweller

::

:: Received August 29, 2019

:: Copyright (c) 2019-2021 Association of Mizar Users

Th1: for R being Ring holds R is Subring of R

by LIOUVIL2:18;

registration

let R be non degenerated Ring;

coherence

for b_{1} being Subring of R holds not b_{1} is degenerated

end;
coherence

for b

proof end;

registration
end;

registration
end;

theorem Th2: :: FIELD_4:2

for R being Ring

for S being Subring of R

for F being FinSequence of R

for G being FinSequence of S st F = G holds

Sum F = Sum G

for S being Subring of R

for F being FinSequence of R

for G being FinSequence of S st F = G holds

Sum F = Sum G

proof end;

definition
end;

:: deftheorem Def1 defines -extending FIELD_4:def 1 :

for R, S being Ring holds

( S is R -extending iff R is Subring of S );

for R, S being Ring holds

( S is R -extending iff R is Subring of S );

registration

let R be Ring;

ex b_{1} being Ring st b_{1} is R -extending

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative V201() V202() V203() V204() INT.Ring -homomorphic INT.Ring -homomorphic R -extending for doubleLoopStr ;

existence ex b

proof end;

registration

let R be comRing;

ex b_{1} being comRing st b_{1} is R -extending

end;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative commutative V201() V202() V203() V204() INT.Ring -homomorphic R -extending for doubleLoopStr ;

existence ex b

proof end;

registration

let R be domRing;

ex b_{1} being domRing st b_{1} is R -extending

end;
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 right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative commutative domRing-like V201() V202() V203() V204() INT.Ring -homomorphic R -extending for doubleLoopStr ;

existence ex b

proof end;

registration

let F be Field;

ex b_{1} being Field st b_{1} is F -extending

end;
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 right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative commutative domRing-like V201() V202() V203() V204() PID V239() Euclidian INT.Ring -homomorphic factorial F -extending for doubleLoopStr ;

existence ex b

proof end;

registration
end;

registration

let R be Ring;

let S be RingExtension of R;

for b_{1} being RingExtension of S holds b_{1} is R -extending

end;
let S be RingExtension of R;

cluster non empty right_complementable well-unital V113() Abelian add-associative right_zeroed associative S -extending -> R -extending for doubleLoopStr ;

coherence for b

proof end;

registration

let R be comRing;

let S be comRingExtension of R;

for b_{1} being comRingExtension of S holds b_{1} is R -extending
;

end;
let S be comRingExtension of R;

cluster non empty right_complementable well-unital V113() Abelian add-associative right_zeroed associative commutative S -extending -> R -extending for doubleLoopStr ;

coherence for b

registration

let R be domRing;

let S be domRingExtension of R;

for b_{1} being domRingExtension of S holds b_{1} is R -extending
;

end;
let S be domRingExtension of R;

cluster non empty non degenerated right_complementable well-unital V113() Abelian add-associative right_zeroed associative commutative domRing-like S -extending -> R -extending for doubleLoopStr ;

coherence for b

registration

let F be Field;

let E be FieldExtension of F;

for b_{1} being FieldExtension of E holds b_{1} is F -extending
;

end;
let E be FieldExtension of F;

cluster non empty non degenerated right_complementable almost_left_invertible well-unital V113() Abelian add-associative right_zeroed associative commutative E -extending -> F -extending for doubleLoopStr ;

coherence for b

registration

let R be non degenerated Ring;

for b_{1} being RingExtension of R holds not b_{1} is degenerated

end;
cluster non empty right_complementable well-unital V113() Abelian add-associative right_zeroed associative R -extending -> non degenerated for doubleLoopStr ;

coherence for b

proof end;

theorem Th5: :: FIELD_4:8

for R being Ring

for S being RingExtension of R

for p being Polynomial of R holds p is Polynomial of S

for S being RingExtension of R

for p being Polynomial of R holds p is Polynomial of S

proof end;

theorem Th6: :: FIELD_4:10

for R being Ring

for S being RingExtension of R holds the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S)

for S being RingExtension of R holds the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S)

proof end;

theorem Th10: :: FIELD_4:15

for R being Ring

for S being RingExtension of R

for p, q being Polynomial of R

for p1, q1 being Polynomial of S st p = p1 & q = q1 holds

p + q = p1 + q1

for S being RingExtension of R

for p, q being Polynomial of R

for p1, q1 being Polynomial of S st p = p1 & q = q1 holds

p + q = p1 + q1

proof end;

theorem Th11: :: FIELD_4:16

for R being Ring

for S being RingExtension of R holds the addF of (Polynom-Ring R) = the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)

for S being RingExtension of R holds the addF of (Polynom-Ring R) = the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)

proof end;

theorem Th12: :: FIELD_4:17

for R being Ring

for S being RingExtension of R

for p, q being Polynomial of R

for p1, q1 being Polynomial of S st p = p1 & q = q1 holds

p *' q = p1 *' q1

for S being RingExtension of R

for p, q being Polynomial of R

for p1, q1 being Polynomial of S st p = p1 & q = q1 holds

p *' q = p1 *' q1

proof end;

theorem Th13: :: FIELD_4:18

for R, S being Ring st S is RingExtension of R holds

the multF of (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)

the multF of (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)

proof end;

registration

let R be Ring;

let S be RingExtension of R;

coherence

Polynom-Ring S is Polynom-Ring R -extending

end;
let S be RingExtension of R;

coherence

Polynom-Ring S is Polynom-Ring R -extending

proof end;

theorem :: FIELD_4:19

for R being Ring

for S being RingExtension of R holds Polynom-Ring S is RingExtension of Polynom-Ring R ;

for S being RingExtension of R holds Polynom-Ring S is RingExtension of Polynom-Ring R ;

theorem :: FIELD_4:20

for R being Ring

for S being RingExtension of R

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

for q being Element of the carrier of (Polynom-Ring S) st p = q holds

deg p = deg q

for S being RingExtension of R

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

for q being Element of the carrier of (Polynom-Ring S) st p = q holds

deg p = deg q

proof end;

Lm2: for R being Ring

for S being RingExtension of R

for a being Element of R

for b being Element of S st a = b holds

- a = - b

proof end;

theorem :: FIELD_4:21

for R being non degenerated Ring

for S being RingExtension of R

for a being Element of R

for b being Element of S st a = b holds

rpoly (1,a) = rpoly (1,b)

for S being RingExtension of R

for a being Element of R

for b being Element of S st a = b holds

rpoly (1,a) = rpoly (1,b)

proof end;

theorem :: FIELD_4:22

for R, S being Ring

for a being Element of S st S is RingExtension of R holds

Ext_eval ((0_. R),a) = 0. S by ALGNUM_1:13;

for a being Element of S st S is RingExtension of R holds

Ext_eval ((0_. R),a) = 0. S by ALGNUM_1:13;

theorem :: FIELD_4:23

for R being non degenerated Ring

for S being RingExtension of R

for a being Element of S holds Ext_eval ((1_. R),a) = 1. S

for S being RingExtension of R

for a being Element of S holds Ext_eval ((1_. R),a) = 1. S

proof end;

theorem :: FIELD_4:24

for R being Ring

for S being RingExtension of R

for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

for S being RingExtension of R

for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))

proof end;

theorem :: FIELD_4:25

for R being comRing

for S being comRingExtension of R

for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p *' q),a) = (Ext_eval (p,a)) * (Ext_eval (q,a))

for S being comRingExtension of R

for a being Element of S

for p, q being Polynomial of R holds Ext_eval ((p *' q),a) = (Ext_eval (p,a)) * (Ext_eval (q,a))

proof end;

Th14: for R being Ring

for S being RingExtension of R

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

for a being Element of R

for b being Element of S st b = a holds

Ext_eval (p,b) = eval (p,a)

proof end;

theorem Th15: :: FIELD_4:26

for R being Ring

for S being RingExtension of R

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

for q being Element of the carrier of (Polynom-Ring S)

for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

for S being RingExtension of R

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

for q being Element of the carrier of (Polynom-Ring S)

for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

proof end;

theorem :: FIELD_4:27

for R being Ring

for S being RingExtension of R

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

for q being Element of the carrier of (Polynom-Ring S)

for a being Element of R

for b being Element of S st q = p & b = a holds

eval (q,b) = eval (p,a)

for S being RingExtension of R

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

for q being Element of the carrier of (Polynom-Ring S)

for a being Element of R

for b being Element of S st q = p & b = a holds

eval (q,b) = eval (p,a)

proof end;

definition

let R be Ring;

let S be RingExtension of R;

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

let a be Element of S;

end;
let S be RingExtension of R;

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

let a be Element of S;

:: deftheorem defines is_a_root_of FIELD_4:def 2 :

for R being Ring

for S being RingExtension of R

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

for a being Element of S holds

( a is_a_root_of p,S iff Ext_eval (p,a) = 0. S );

for R being Ring

for S being RingExtension of R

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

for a being Element of S holds

( a is_a_root_of p,S iff Ext_eval (p,a) = 0. S );

definition
end;

:: deftheorem defines is_with_roots_in FIELD_4:def 3 :

for R being Ring

for S being RingExtension of R

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

( p is_with_roots_in S iff ex a being Element of S st a is_a_root_of p,S );

for R being Ring

for S being RingExtension of R

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

( p is_with_roots_in S iff ex a being Element of S st a is_a_root_of p,S );

definition

let R be Ring;

let S be RingExtension of R;

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

{ a where a is Element of S : a is_a_root_of p,S } is Subset of S

end;
let S be RingExtension of R;

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

func Roots (S,p) -> Subset of S equals :: FIELD_4:def 4

{ a where a is Element of S : a is_a_root_of p,S } ;

coherence { a where a is Element of S : a is_a_root_of p,S } ;

{ a where a is Element of S : a is_a_root_of p,S } is Subset of S

proof end;

:: deftheorem defines Roots FIELD_4:def 4 :

for R being Ring

for S being RingExtension of R

for p being Element of the carrier of (Polynom-Ring R) holds Roots (S,p) = { a where a is Element of S : a is_a_root_of p,S } ;

for R being Ring

for S being RingExtension of R

for p being Element of the carrier of (Polynom-Ring R) holds Roots (S,p) = { a where a is Element of S : a is_a_root_of p,S } ;

theorem :: FIELD_4:28

for R being Ring

for S being RingExtension of R

for p being Element of the carrier of (Polynom-Ring R) holds Roots p c= Roots (S,p)

for S being RingExtension of R

for p being Element of the carrier of (Polynom-Ring R) holds Roots p c= Roots (S,p)

proof end;

::: changed Element of the carrier of Polynom-Ring R -> Polynomial R

:: deftheorem defines splits_in FIELD_4:def 5 :

for R being Ring

for S being non degenerated Ring

for p being Polynomial of R holds

( p splits_in S iff ex a being non zero Element of S ex q being Ppoly of S st p = a * q );

for R being Ring

for S being non degenerated Ring

for p being Polynomial of R holds

( p splits_in S iff ex a being non zero Element of S ex q being Ppoly of S st p = a * q );

::: changed Element of the carrier of Polynom-Ring R -> Polynomial R

definition

let R be Ring;

let S be RingExtension of R;

ex b_{1} being strict ModuleStr over R st

( the carrier of b_{1} = the carrier of S & the addF of b_{1} = the addF of S & the ZeroF of b_{1} = 0. S & the lmult of b_{1} = the multF of S | [: the carrier of R, the carrier of S:] )

for b_{1}, b_{2} being strict ModuleStr over R st the carrier of b_{1} = the carrier of S & the addF of b_{1} = the addF of S & the ZeroF of b_{1} = 0. S & the lmult of b_{1} = the multF of S | [: the carrier of R, the carrier of S:] & the carrier of b_{2} = the carrier of S & the addF of b_{2} = the addF of S & the ZeroF of b_{2} = 0. S & the lmult of b_{2} = the multF of S | [: the carrier of R, the carrier of S:] holds

b_{1} = b_{2}
;

end;
let S be RingExtension of R;

func VecSp (S,R) -> strict ModuleStr over R means :Def5: :: FIELD_4:def 6

( the carrier of it = the carrier of S & the addF of it = the addF of S & the ZeroF of it = 0. S & the lmult of it = the multF of S | [: the carrier of R, the carrier of S:] );

existence ( the carrier of it = the carrier of S & the addF of it = the addF of S & the ZeroF of it = 0. S & the lmult of it = the multF of S | [: the carrier of R, the carrier of S:] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines VecSp FIELD_4:def 6 :

for R being Ring

for S being RingExtension of R

for b_{3} being strict ModuleStr over R holds

( b_{3} = VecSp (S,R) iff ( the carrier of b_{3} = the carrier of S & the addF of b_{3} = the addF of S & the ZeroF of b_{3} = 0. S & the lmult of b_{3} = the multF of S | [: the carrier of R, the carrier of S:] ) );

for R being Ring

for S being RingExtension of R

for b

( b

registration
end;

registration

let R be Ring;

let S be RingExtension of R;

coherence

( VecSp (S,R) is Abelian & VecSp (S,R) is add-associative & VecSp (S,R) is right_zeroed & VecSp (S,R) is right_complementable )

end;
let S be RingExtension of R;

coherence

( VecSp (S,R) is Abelian & VecSp (S,R) is add-associative & VecSp (S,R) is right_zeroed & VecSp (S,R) is right_complementable )

proof end;

Lm3: for R being Ring

for E being RingExtension of R

for a, b being Element of E

for s being Element of R

for v being Element of (VecSp (E,R)) st a = s & b = v holds

a * b = s * v

proof end;

Lm4: for R being Ring

for E being RingExtension of R

for a, b being Element of E

for x, y being Element of R st a = x & b = y holds

a + b = x + y

proof end;

Lm5: for R being Ring

for E being RingExtension of R

for a, b being Element of E

for x, y being Element of R st a = x & b = y holds

a * b = x * y

proof end;

registration

let R be Ring;

let S be RingExtension of R;

( VecSp (S,R) is scalar-distributive & VecSp (S,R) is scalar-associative & VecSp (S,R) is scalar-unital & VecSp (S,R) is vector-distributive )

end;
let S be RingExtension of R;

cluster VecSp (S,R) -> strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( VecSp (S,R) is scalar-distributive & VecSp (S,R) is scalar-associative & VecSp (S,R) is scalar-unital & VecSp (S,R) is vector-distributive )

proof end;

theorem :: FIELD_4:30

definition

let F be Field;

let E be FieldExtension of F;

( ( VecSp (E,F) is finite-dimensional implies dim (VecSp (E,F)) is Integer ) & ( not VecSp (E,F) is finite-dimensional implies - 1 is Integer ) ) ;

consistency

for b_{1} being Integer holds verum
;

end;
let E be FieldExtension of F;

func deg (E,F) -> Integer equals :Def6: :: FIELD_4:def 7

dim (VecSp (E,F)) if VecSp (E,F) is finite-dimensional

otherwise - 1;

coherence dim (VecSp (E,F)) if VecSp (E,F) is finite-dimensional

otherwise - 1;

( ( VecSp (E,F) is finite-dimensional implies dim (VecSp (E,F)) is Integer ) & ( not VecSp (E,F) is finite-dimensional implies - 1 is Integer ) ) ;

consistency

for b

:: deftheorem Def6 defines deg FIELD_4:def 7 :

for F being Field

for E being FieldExtension of F holds

( ( VecSp (E,F) is finite-dimensional implies deg (E,F) = dim (VecSp (E,F)) ) & ( not VecSp (E,F) is finite-dimensional implies deg (E,F) = - 1 ) );

for F being Field

for E being FieldExtension of F holds

( ( VecSp (E,F) is finite-dimensional implies deg (E,F) = dim (VecSp (E,F)) ) & ( not VecSp (E,F) is finite-dimensional implies deg (E,F) = - 1 ) );

registration
end;

:: deftheorem Def7 defines -finite FIELD_4:def 8 :

for F being Field

for E being FieldExtension of F holds

( E is F -finite iff VecSp (E,F) is finite-dimensional );

for F being Field

for E being FieldExtension of F holds

( E is F -finite iff VecSp (E,F) is finite-dimensional );

registration

let F be Field;

ex b_{1} being FieldExtension of F st b_{1} is F -finite

end;
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 right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative commutative domRing-like V201() V202() V203() V204() PID V239() Euclidian INT.Ring -homomorphic factorial F -extending F -finite for doubleLoopStr ;

existence ex b

proof end;

registration
end;

registration

let F be Field;

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

coherence

the carrier of (Polynom-Ring p) is F -polynomial-membered

Polynom-Ring p is F -polynomial-membered ;

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

coherence

the carrier of (Polynom-Ring p) is F -polynomial-membered

proof end;

coherence Polynom-Ring p is F -polynomial-membered ;

definition

let F be Field;

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

ex b_{1} being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) st

for q being Element of the carrier of (Polynom-Ring p) holds b_{1} . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q)

for b_{1}, b_{2} being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) st ( for q being Element of the carrier of (Polynom-Ring p) holds b_{1} . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) ) & ( for q being Element of the carrier of (Polynom-Ring p) holds b_{2} . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) ) holds

b_{1} = b_{2}

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

func KroneckerIso p -> Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) means :Def8: :: FIELD_4:def 9

for q being Element of the carrier of (Polynom-Ring p) holds it . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q);

existence for q being Element of the carrier of (Polynom-Ring p) holds it . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q);

ex b

for q being Element of the carrier of (Polynom-Ring p) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines KroneckerIso FIELD_4:def 9 :

for F being Field

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

for b_{3} being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) holds

( b_{3} = KroneckerIso p iff for q being Element of the carrier of (Polynom-Ring p) holds b_{3} . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) );

for F being Field

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

for b

( b

Lm6: for L being Ring

for a being Element of (Polynom-Ring L)

for p being Polynomial of L st a = p holds

- a = - p

proof end;

Lm7: for L being Ring

for a, b being Element of (Polynom-Ring L)

for p, q being Polynomial of L st a = p & b = q holds

a - b = p - q

proof end;

Lm8: for F being Field

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

for a being Element of (Polynom-Ring p) holds a in the carrier of (Polynom-Ring F)

proof end;

Lm9: for F being Field

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

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

for q being Element of (Polynom-Ring p) st a = q holds

- a = - q

proof end;

Lm10: for F being Field

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

for a, b being Element of the carrier of (Polynom-Ring F)

for q, r being Element of (Polynom-Ring p) st a = q & b = r holds

a - b = q - r

proof end;

registration

let F be Field;

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

coherence

( KroneckerIso p is additive & KroneckerIso p is multiplicative & KroneckerIso p is unity-preserving & KroneckerIso p is one-to-one & KroneckerIso p is onto )

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

coherence

( KroneckerIso p is additive & KroneckerIso p is multiplicative & KroneckerIso p is unity-preserving & KroneckerIso p is one-to-one & KroneckerIso p is onto )

proof end;

registration

let F be Field;

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

( KroneckerField (F,p) is Polynom-Ring p -homomorphic & KroneckerField (F,p) is Polynom-Ring p -monomorphic & KroneckerField (F,p) is Polynom-Ring p -isomorphic )

( Polynom-Ring p is KroneckerField (F,p) -homomorphic & Polynom-Ring p is KroneckerField (F,p) -monomorphic & Polynom-Ring p is KroneckerField (F,p) -isomorphic )

( Polynom-Ring p is F -homomorphic & Polynom-Ring p is F -monomorphic ) ;

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

cluster KroneckerField (F,p) -> Polynom-Ring p -homomorphic Polynom-Ring p -monomorphic Polynom-Ring p -isomorphic ;

coherence ( KroneckerField (F,p) is Polynom-Ring p -homomorphic & KroneckerField (F,p) is Polynom-Ring p -monomorphic & KroneckerField (F,p) is Polynom-Ring p -isomorphic )

proof end;

cluster Polynom-Ring p -> KroneckerField (F,p) -homomorphic KroneckerField (F,p) -monomorphic KroneckerField (F,p) -isomorphic ;

coherence ( Polynom-Ring p is KroneckerField (F,p) -homomorphic & Polynom-Ring p is KroneckerField (F,p) -monomorphic & Polynom-Ring p is KroneckerField (F,p) -isomorphic )

proof end;

coherence ( Polynom-Ring p is F -homomorphic & Polynom-Ring p is F -monomorphic ) ;

Lm11: for F being polynomial_disjoint Field

for p being irreducible Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st p is_with_roots_in E

proof end;

theorem :: FIELD_4:31

for F being polynomial_disjoint Field

for f being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st f is_with_roots_in E

for f being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st f is_with_roots_in E

proof end;