:: by Christoph Schwarzweller

::

:: Received May 19, 2020

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

theorem th0k: :: FIELD_5:3

for n, m being Nat holds

( ( n c= m implies n <= m ) & ( n <= m implies n c= m ) & ( n in m implies n < m ) & ( n < m implies n in m ) )

( ( n c= m implies n <= m ) & ( n <= m implies n c= m ) & ( n in m implies n < m ) & ( n < m implies n in m ) )

proof end;

registration

let F be Field;

let E be FieldExtension of F;

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

end;
let E be FieldExtension of F;

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 V115() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like V217() V278() V279() V280() V281() PID Euclidian INT.Ring -homomorphic factorial F -extending E -extending for doubleLoopStr ;

existence ex b

proof end;

theorem sp: :: FIELD_5:14

for F being Field

for E being FieldExtension of F

for K being b_{2} -extending FieldExtension of F holds VecSp (E,F) is Subspace of VecSp (K,F)

for E being FieldExtension of F

for K being b

proof end;

theorem :: FIELD_5:15

for F being Field

for E being FieldExtension of F

for K being b_{2} -extending FieldExtension of F holds

( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )

for E being FieldExtension of F

for K being b

( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )

proof end;

theorem divmod: :: FIELD_5:16

for F being Field

for p being Polynomial of F

for q being non zero Polynomial of F holds deg (p mod q) < deg q

for p being Polynomial of F

for q being non zero Polynomial of F holds deg (p mod q) < deg q

proof end;

lempk: for F, K being Field st the carrier of F = the carrier of K & 0. F = 0. K holds

the carrier of (Polynom-Ring F) = the carrier of (Polynom-Ring K)

proof end;

definition
end;

:: deftheorem defl defines linear FIELD_5:def 1 :

for R being Ring

for p being Polynomial of R holds

( p is linear iff deg p = 1 );

for R being Ring

for p being Polynomial of R holds

( p is linear iff deg p = 1 );

registration

let R be non degenerated Ring;

ex b_{1} being Polynomial of R st b_{1} is linear

not for b_{1} being Polynomial of R holds b_{1} is linear

ex b_{1} being Element of the carrier of (Polynom-Ring R) st b_{1} is linear

not for b_{1} being Element of the carrier of (Polynom-Ring R) holds b_{1} is linear

end;
cluster non empty Relation-like omega -defined the carrier of R -valued Function-like V27( omega ) quasi_total finite-Support linear for Element of bool [:omega, the carrier of R:];

existence ex b

proof end;

cluster non empty Relation-like omega -defined the carrier of R -valued Function-like V27( omega ) quasi_total finite-Support non linear for Element of bool [:omega, the carrier of R:];

existence not for b

proof end;

cluster non empty Relation-like omega -defined the carrier of R -valued Function-like V27( omega ) quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support linear for Element of the carrier of (Polynom-Ring R);

existence ex b

proof end;

cluster non empty Relation-like omega -defined the carrier of R -valued Function-like V27( omega ) quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support non linear for Element of the carrier of (Polynom-Ring R);

existence not for b

proof end;

registration

let R be non degenerated Ring;

for b_{1} being Polynomial of R st b_{1} is zero holds

not b_{1} is linear

for b_{1} being Polynomial of R st b_{1} is constant holds

not b_{1} is linear
by RATFUNC1:def 2;

end;
cluster Function-like quasi_total finite-Support zero -> non linear for Element of bool [:omega, the carrier of R:];

coherence for b

not b

proof end;

cluster Function-like quasi_total finite-Support constant -> non linear for Element of bool [:omega, the carrier of R:];

coherence for b

not b

registration

let F be Field;

for b_{1} being Polynomial of F st b_{1} is linear holds

b_{1} is with_roots

end;
cluster Function-like quasi_total finite-Support linear -> with_roots for Element of bool [:omega, the carrier of F:];

coherence for b

b

proof end;

registration

let F be Field;

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F) st b_{1} is linear holds

b_{1} is irreducible
by RING_4:44;

end;
coherence

for b

b

registration

let F be Field;

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F) st not b_{1} is linear & b_{1} is with_roots holds

b_{1} is reducible

end;
coherence

for b

b

proof end;

registration

let R be domRing;

let p be linear Polynomial of R;

let q be non constant Polynomial of R;

coherence

not p *' q is linear

end;
let p be linear Polynomial of R;

let q be non constant Polynomial of R;

coherence

not p *' q is linear

proof end;

registration

let F be Field;

let p be linear Polynomial of F;

let q be non constant Polynomial of F;

coherence

p *' q is with_roots ;

end;
let p be linear Polynomial of F;

let q be non constant Polynomial of F;

coherence

p *' q is with_roots ;

lemdis: for F being polynomial_disjoint Field

for p being non constant Element of the carrier of (Polynom-Ring F) holds F, Polynom-Ring p are_disjoint

proof end;

definition

let F be Field;

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

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

for a being Element of F holds b_{1} . a = a | F

for b_{1}, b_{2} being Function of F,(Polynom-Ring p) st ( for a being Element of F holds b_{1} . a = a | F ) & ( for a being Element of F holds b_{2} . a = a | F ) holds

b_{1} = b_{2}

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

func canHomP p -> Function of F,(Polynom-Ring p) means :defch: :: FIELD_5:def 2

for a being Element of F holds it . a = a | F;

existence for a being Element of F holds it . a = a | F;

ex b

for a being Element of F holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defch defines canHomP FIELD_5:def 2 :

for F being Field

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

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

( b_{3} = canHomP p iff for a being Element of F holds b_{3} . a = a | F );

for F being Field

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

for b

( b

registration

let F be Field;

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

coherence

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

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

coherence

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

proof end;

registration

let F be Field;

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

coherence

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

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

coherence

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

proof end;

registration

let F be polynomial_disjoint Field;

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

( embField (canHomP p) is add-associative & embField (canHomP p) is right_complementable & embField (canHomP p) is associative & embField (canHomP p) is distributive & embField (canHomP p) is almost_left_invertible ) by lemdis, FIELD_2:12;

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

cluster embField (canHomP p) -> right_complementable almost_left_invertible add-associative distributive associative ;

coherence ( embField (canHomP p) is add-associative & embField (canHomP p) is right_complementable & embField (canHomP p) is associative & embField (canHomP p) is distributive & embField (canHomP p) is almost_left_invertible ) by lemdis, FIELD_2:12;

registration

let F be polynomial_disjoint Field;

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

coherence

embField (canHomP p) is F -extending

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

coherence

embField (canHomP p) is F -extending

proof end;

definition

let F be polynomial_disjoint Field;

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

(((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p) is Element of (embField (canHomP p))

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

func KrRootP p -> Element of (embField (canHomP p)) equals :: FIELD_5:def 3

(((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p);

coherence (((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p);

(((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p) is Element of (embField (canHomP p))

proof end;

:: deftheorem defines KrRootP FIELD_5:def 3 :

for F being polynomial_disjoint Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRootP p = (((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p);

for F being polynomial_disjoint Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRootP p = (((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p);

theorem :: FIELD_5:17

for F being polynomial_disjoint Field

for p being irreducible Element of the carrier of (Polynom-Ring F) holds Ext_eval (p,(KrRootP p)) = 0. F

for p being irreducible Element of the carrier of (Polynom-Ring F) holds Ext_eval (p,(KrRootP p)) = 0. F

proof end;

theorem polyd: :: FIELD_5:18

for F being Field

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

( Polynom-Ring p,F are_isomorphic & the carrier of (embField (canHomP p)) = the carrier of F )

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

( Polynom-Ring p,F are_isomorphic & the carrier of (embField (canHomP p)) = the carrier of F )

proof end;

theorem :: FIELD_5:19

for F being strict Field

for p being linear Element of the carrier of (Polynom-Ring F) holds embField (canHomP p) = F

for p being linear Element of the carrier of (Polynom-Ring F) holds embField (canHomP p) = F

proof end;

theorem polyd1: :: FIELD_5:20

for F being Field

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

( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )

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

( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )

proof end;

theorem :: FIELD_5:21

for F being strict Field

for p being linear Element of the carrier of (Polynom-Ring F) holds embField (emb p) = F

for p being linear Element of the carrier of (Polynom-Ring F) holds embField (emb p) = F

proof end;

theorem :: FIELD_5:22

for F being polynomial_disjoint Field

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

( embField (canHomP p) is polynomial_disjoint iff p is linear )

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

( embField (canHomP p) is polynomial_disjoint iff p is linear )

proof end;

theorem :: FIELD_5:23

for F being Field

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

for E being polynomial_disjoint Field st E = embField (emb p) holds

F is polynomial_disjoint

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

for E being polynomial_disjoint Field st E = embField (emb p) holds

F is polynomial_disjoint

proof end;

Disj1: for n being non trivial Nat

for p being Element of the carrier of (Polynom-Ring (Z/ n)) holds the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) = {}

proof end;

Disj2: for p being Element of the carrier of (Polynom-Ring F_Rat) holds the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) = {}

proof end;

registration

let n be Prime;

let p be irreducible Element of the carrier of (Polynom-Ring (Z/ n));

( embField (emb p) is add-associative & embField (emb p) is right_complementable & embField (emb p) is associative & embField (emb p) is distributive & embField (emb p) is almost_left_invertible )

end;
let p be irreducible Element of the carrier of (Polynom-Ring (Z/ n));

cluster embField (emb p) -> right_complementable almost_left_invertible add-associative distributive associative ;

coherence ( embField (emb p) is add-associative & embField (emb p) is right_complementable & embField (emb p) is associative & embField (emb p) is distributive & embField (emb p) is almost_left_invertible )

proof end;

registration

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

( embField (emb p) is add-associative & embField (emb p) is right_complementable & embField (emb p) is associative & embField (emb p) is distributive & embField (emb p) is almost_left_invertible )

end;
cluster embField (emb p) -> right_complementable almost_left_invertible add-associative distributive associative ;

coherence ( embField (emb p) is add-associative & embField (emb p) is right_complementable & embField (emb p) is associative & embField (emb p) is distributive & embField (emb p) is almost_left_invertible )

proof end;

theorem :: FIELD_5:24

for n being Prime

for p being non constant Element of the carrier of (Polynom-Ring (Z/ n)) holds Z/ n,(Polynom-Ring (Z/ n)) / ({p} -Ideal) are_disjoint

for p being non constant Element of the carrier of (Polynom-Ring (Z/ n)) holds Z/ n,(Polynom-Ring (Z/ n)) / ({p} -Ideal) are_disjoint

proof end;

theorem :: FIELD_5:25

for p being non constant Element of the carrier of (Polynom-Ring F_Rat) holds F_Rat ,(Polynom-Ring F_Rat) / ({p} -Ideal) are_disjoint

proof end;

registration

let n be Prime;

let p be irreducible Element of the carrier of (Polynom-Ring (Z/ n));

coherence

embField (emb p) is polynomial_disjoint

end;
let p be irreducible Element of the carrier of (Polynom-Ring (Z/ n));

coherence

embField (emb p) is polynomial_disjoint

proof end;

registration

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

coherence

embField (emb p) is polynomial_disjoint

end;
coherence

embField (emb p) is polynomial_disjoint

proof end;

definition

let R be Ring;

end;
attr R is strong_polynomial_disjoint means :dspd: :: FIELD_5:def 4

for a being Element of R

for S being Ring

for p being Element of the carrier of (Polynom-Ring S) holds a <> p;

for a being Element of R

for S being Ring

for p being Element of the carrier of (Polynom-Ring S) holds a <> p;

:: deftheorem dspd defines strong_polynomial_disjoint FIELD_5:def 4 :

for R being Ring holds

( R is strong_polynomial_disjoint iff for a being Element of R

for S being Ring

for p being Element of the carrier of (Polynom-Ring S) holds a <> p );

for R being Ring holds

( R is strong_polynomial_disjoint iff for a being Element of R

for S being Ring

for p being Element of the carrier of (Polynom-Ring S) holds a <> p );

registration

coherence

INT.Ring is strong_polynomial_disjoint by FIELD_3:25;

coherence

F_Rat is strong_polynomial_disjoint by FIELD_3:25;

coherence

F_Real is strong_polynomial_disjoint by FIELD_3:26;

end;
INT.Ring is strong_polynomial_disjoint by FIELD_3:25;

coherence

F_Rat is strong_polynomial_disjoint by FIELD_3:25;

coherence

F_Real is strong_polynomial_disjoint by FIELD_3:26;

registration

for b_{1} being Ring st b_{1} is strong_polynomial_disjoint holds

b_{1} is polynomial_disjoint
end;

cluster non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative strong_polynomial_disjoint -> polynomial_disjoint for doubleLoopStr ;

coherence for b

b

proof end;

registration

ex b_{1} being Field st b_{1} is strong_polynomial_disjoint

not for b_{1} being Field holds b_{1} is strong_polynomial_disjoint
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 Abelian add-associative right_zeroed V115() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like V217() V278() V279() V280() V281() PID Euclidian INT.Ring -homomorphic factorial strong_polynomial_disjoint for doubleLoopStr ;

existence ex b

proof 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 Abelian add-associative right_zeroed V115() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like V217() V278() V279() V280() V281() PID Euclidian INT.Ring -homomorphic factorial non strong_polynomial_disjoint for doubleLoopStr ;

existence not for b

proof end;

theorem :: FIELD_5:26

for F being strong_polynomial_disjoint Field

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

for E being Field st E = embField (emb p) holds

E is strong_polynomial_disjoint

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

for E being Field st E = embField (emb p) holds

E is strong_polynomial_disjoint

proof end;

definition

let X be non empty set ;

let Z be set ;

ex b_{1} being Function st

( dom b_{1} = X & b_{1} is one-to-one & (rng b_{1}) /\ (X \/ Z) = {} )

end;
let Z be set ;

mode Renaming of X,Z -> Function means :defr: :: FIELD_5:def 5

( dom it = X & it is one-to-one & (rng it) /\ (X \/ Z) = {} );

existence ( dom it = X & it is one-to-one & (rng it) /\ (X \/ Z) = {} );

ex b

( dom b

proof end;

:: deftheorem defr defines Renaming FIELD_5:def 5 :

for X being non empty set

for Z being set

for b_{3} being Function holds

( b_{3} is Renaming of X,Z iff ( dom b_{3} = X & b_{3} is one-to-one & (rng b_{3}) /\ (X \/ Z) = {} ) );

for X being non empty set

for Z being set

for b

( b

registration

let X be non empty set ;

let Z be set ;

let r be Renaming of X,Z;

coherence

not dom r is empty by defr;

coherence

not rng r is empty

end;
let Z be set ;

let r be Renaming of X,Z;

coherence

not dom r is empty by defr;

coherence

not rng r is empty

proof end;

registration

let X be non empty set ;

let Z be set ;

coherence

for b_{1} being Renaming of X,Z holds

( b_{1} is X -defined & b_{1} is one-to-one )

end;
let Z be set ;

coherence

for b

( b

proof end;

definition

let X be non empty set ;

let Z be set ;

let r be Renaming of X,Z;

:: original: "

redefine func r " -> Function of (rng r),X;

coherence

r " is Function of (rng r),X

end;
let Z be set ;

let r be Renaming of X,Z;

:: original: "

redefine func r " -> Function of (rng r),X;

coherence

r " is Function of (rng r),X

proof end;

definition

let F be Field;

let Z be set ;

let r be Renaming of the carrier of F,Z;

ex b_{1} being BinOp of (rng r) st

for a, b being Element of rng r holds b_{1} . (a,b) = r . (((r ") . a) + ((r ") . b))

for b_{1}, b_{2} being BinOp of (rng r) st ( for a, b being Element of rng r holds b_{1} . (a,b) = r . (((r ") . a) + ((r ") . b)) ) & ( for a, b being Element of rng r holds b_{2} . (a,b) = r . (((r ") . a) + ((r ") . b)) ) holds

b_{1} = b_{2}

end;
let Z be set ;

let r be Renaming of the carrier of F,Z;

func ren_add r -> BinOp of (rng r) means :defra: :: FIELD_5:def 6

for a, b being Element of rng r holds it . (a,b) = r . (((r ") . a) + ((r ") . b));

existence for a, b being Element of rng r holds it . (a,b) = r . (((r ") . a) + ((r ") . b));

ex b

for a, b being Element of rng r holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defra defines ren_add FIELD_5:def 6 :

for F being Field

for Z being set

for r being Renaming of the carrier of F,Z

for b_{4} being BinOp of (rng r) holds

( b_{4} = ren_add r iff for a, b being Element of rng r holds b_{4} . (a,b) = r . (((r ") . a) + ((r ") . b)) );

for F being Field

for Z being set

for r being Renaming of the carrier of F,Z

for b

( b

definition

let F be Field;

let Z be set ;

let r be Renaming of the carrier of F,Z;

ex b_{1} being BinOp of (rng r) st

for a, b being Element of rng r holds b_{1} . (a,b) = r . (((r ") . a) * ((r ") . b))

for b_{1}, b_{2} being BinOp of (rng r) st ( for a, b being Element of rng r holds b_{1} . (a,b) = r . (((r ") . a) * ((r ") . b)) ) & ( for a, b being Element of rng r holds b_{2} . (a,b) = r . (((r ") . a) * ((r ") . b)) ) holds

b_{1} = b_{2}

end;
let Z be set ;

let r be Renaming of the carrier of F,Z;

func ren_mult r -> BinOp of (rng r) means :defrm: :: FIELD_5:def 7

for a, b being Element of rng r holds it . (a,b) = r . (((r ") . a) * ((r ") . b));

existence for a, b being Element of rng r holds it . (a,b) = r . (((r ") . a) * ((r ") . b));

ex b

for a, b being Element of rng r holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defrm defines ren_mult FIELD_5:def 7 :

for F being Field

for Z being set

for r being Renaming of the carrier of F,Z

for b_{4} being BinOp of (rng r) holds

( b_{4} = ren_mult r iff for a, b being Element of rng r holds b_{4} . (a,b) = r . (((r ") . a) * ((r ") . b)) );

for F being Field

for Z being set

for r being Renaming of the carrier of F,Z

for b

( b

definition

let F be Field;

let Z be set ;

let r be Renaming of the carrier of F,Z;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = rng r & the addF of b_{1} = ren_add r & the multF of b_{1} = ren_mult r & the OneF of b_{1} = r . (1. F) & the ZeroF of b_{1} = r . (0. F) )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = rng r & the addF of b_{1} = ren_add r & the multF of b_{1} = ren_mult r & the OneF of b_{1} = r . (1. F) & the ZeroF of b_{1} = r . (0. F) & the carrier of b_{2} = rng r & the addF of b_{2} = ren_add r & the multF of b_{2} = ren_mult r & the OneF of b_{2} = r . (1. F) & the ZeroF of b_{2} = r . (0. F) holds

b_{1} = b_{2}
;

end;
let Z be set ;

let r be Renaming of the carrier of F,Z;

func RenField r -> strict doubleLoopStr means :defrf: :: FIELD_5:def 8

( the carrier of it = rng r & the addF of it = ren_add r & the multF of it = ren_mult r & the OneF of it = r . (1. F) & the ZeroF of it = r . (0. F) );

existence ( the carrier of it = rng r & the addF of it = ren_add r & the multF of it = ren_mult r & the OneF of it = r . (1. F) & the ZeroF of it = r . (0. F) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defrf defines RenField FIELD_5:def 8 :

for F being Field

for Z being set

for r being Renaming of the carrier of F,Z

for b_{4} being strict doubleLoopStr holds

( b_{4} = RenField r iff ( the carrier of b_{4} = rng r & the addF of b_{4} = ren_add r & the multF of b_{4} = ren_mult r & the OneF of b_{4} = r . (1. F) & the ZeroF of b_{4} = r . (0. F) ) );

for F being Field

for Z being set

for r being Renaming of the carrier of F,Z

for b

( b

registration

let F be Field;

let Z be set ;

let r be Renaming of the carrier of F,Z;

coherence

not RenField r is degenerated

end;
let Z be set ;

let r be Renaming of the carrier of F,Z;

coherence

not RenField r is degenerated

proof end;

registration

let F be Field;

let Z be set ;

let r be Renaming of the carrier of F,Z;

coherence

( RenField r is Abelian & RenField r is add-associative & RenField r is right_zeroed & RenField r is right_complementable )

end;
let Z be set ;

let r be Renaming of the carrier of F,Z;

coherence

( RenField r is Abelian & RenField r is add-associative & RenField r is right_zeroed & RenField r is right_complementable )

proof end;

registration

let F be Field;

let Z be set ;

let r be Renaming of the carrier of F,Z;

( RenField r is commutative & RenField r is associative & RenField r is well-unital & RenField r is distributive & RenField r is almost_left_invertible )

end;
let Z be set ;

let r be Renaming of the carrier of F,Z;

cluster RenField r -> almost_left_invertible strict well-unital distributive associative commutative ;

coherence ( RenField r is commutative & RenField r is associative & RenField r is well-unital & RenField r is distributive & RenField r is almost_left_invertible )

proof end;

definition

let F be Field;

let Z be set ;

let r be Renaming of the carrier of F,Z;

:: original: "

redefine func r " -> Function of (RenField r),F;

coherence

r " is Function of (RenField r),F

end;
let Z be set ;

let r be Renaming of the carrier of F,Z;

:: original: "

redefine func r " -> Function of (RenField r),F;

coherence

r " is Function of (RenField r),F

proof end;

theorem thiso: :: FIELD_5:28

for F being Field

for Z being set

for r being Renaming of the carrier of F,Z holds

( r " is additive & r " is multiplicative & r " is unity-preserving & r " is one-to-one & r " is onto )

for Z being set

for r being Renaming of the carrier of F,Z holds

( r " is additive & r " is multiplicative & r " is unity-preserving & r " is one-to-one & r " is onto )

proof end;

theorem thisofield: :: FIELD_5:29

for F being Field

for Z being set ex E being Field st

( E,F are_isomorphic & the carrier of E /\ ( the carrier of F \/ Z) = {} )

for Z being set ex E being Field st

( E,F are_isomorphic & the carrier of E /\ ( the carrier of F \/ Z) = {} )

proof end;

kron: for F being 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 main: :: FIELD_5:30

for F being 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;

theorem :: FIELD_5:31

for F being Field

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

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

proof end;