and Polynom-Ring(F,p) theorem :: 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; 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; theorem :: 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; 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; theorem :: FIELD_5:22 for F being polynomial_disjoint Field, p being irreducible Element of the carrier of Polynom-Ring F holds embField(canHomP p) is polynomial_disjoint iff p is linear; theorem :: FIELD_5:23 for F being Field, 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; registration let n be Prime; let p be irreducible Element of the carrier of Polynom-Ring(Z/n); cluster embField(emb p) -> add-associative right_complementable associative distributive almost_left_invertible; end; registration let p be irreducible Element of the carrier of Polynom-Ring F_Rat; cluster embField(emb p) -> add-associative right_complementable associative distributive almost_left_invertible; end; theorem :: FIELD_5:24 for n being Prime, p being non constant Element of the carrier of Polynom-Ring(Z/n) holds Z/n, (Polynom-Ring Z/n)/({p}-Ideal) are_disjoint; 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; registration let n be Prime; let p be irreducible Element of the carrier of Polynom-Ring(Z/n); cluster embField(emb p) -> polynomial_disjoint; end; registration let p be irreducible Element of the carrier of Polynom-Ring F_Rat; cluster embField(emb p) -> polynomial_disjoint; end; definition let R be Ring; attr R is strong_polynomial_disjoint means :: FIELD_5:def 4 for a being Element of R for S being Ring, p being Element of the carrier of Polynom-Ring S holds a <> p; end; registration cluster INT.Ring -> strong_polynomial_disjoint; cluster F_Rat -> strong_polynomial_disjoint; cluster F_Real -> strong_polynomial_disjoint; end; registration let n be non trivial Nat; cluster Z/n -> strong_polynomial_disjoint; end; registration cluster strong_polynomial_disjoint -> polynomial_disjoint for Ring; end; registration cluster strong_polynomial_disjoint for Field; cluster non strong_polynomial_disjoint for Field; end; theorem :: FIELD_5:26 for F being strong_polynomial_disjoint Field, 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; begin :: Renamings definition let X be non empty set, Z be set; mode Renaming of X,Z -> Function means :: FIELD_5:def 5 dom it = X & it is one-to-one & (rng it) /\ (X \/ Z) = {}; end; registration let X be non empty set, Z be set; let r be Renaming of X,Z; cluster dom r -> non empty; cluster rng r -> non empty; end; registration let X be non empty set, Z be set; cluster -> X-defined one-to-one for Renaming of X,Z; end; definition let X be non empty set, Z be set; let r be Renaming of X,Z; redefine func r" -> Function of rng r, X; end; theorem :: FIELD_5:27 for X being non empty set, Z being set for r being Renaming of X,Z holds r" is onto; definition let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; func ren_add r -> BinOp of rng r means :: FIELD_5:def 6 for a,b being Element of rng r holds it.(a,b) = r.((r").a + (r").b); end; definition let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; func ren_mult r -> BinOp of (rng r) means :: FIELD_5:def 7 for a,b being Element of (rng r) holds it.(a,b) = r.((r").a * (r").b); end; definition let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; func RenField r -> strict doubleLoopStr means :: 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); end; registration let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; cluster RenField r -> non degenerated; end; registration let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; cluster RenField r -> Abelian add-associative right_zeroed right_complementable; end; registration let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; cluster RenField r -> commutative associative well-unital distributive almost_left_invertible; end; definition let F be Field, Z be set; let r be Renaming of (the carrier of F), Z; redefine func r" -> Function of (RenField r), F; end; theorem :: FIELD_5:28 for F being Field, Z being set for r being Renaming of (the carrier of F), Z holds r" is additive multiplicative unity-preserving one-to-one onto; theorem :: FIELD_5:29 for F being Field, Z being set ex E being Field st E,F are_isomorphic & (the carrier of E) /\ ((the carrier of F) \/ Z) = {}; begin theorem :: FIELD_5:30 :: Kronecker 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; 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;