let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being F1 -algebraic Element of E1
for b being b₁ -algebraic Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)
let F2 be F1 -homomorphic F1 -isomorphic Field; :: thesis: for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being F1 -algebraic Element of E1
for b being F2 -algebraic Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)
let h be Isomorphism of F1,F2; :: thesis: for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being F1 -algebraic Element of E1
for b being F2 -algebraic Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)
let E1 be FieldExtension of F1; :: thesis: for E2 being FieldExtension of F2
for a being F1 -algebraic Element of E1
for b being F2 -algebraic Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)
let E2 be FieldExtension of F2; :: thesis: for a being F1 -algebraic Element of E1
for b being F2 -algebraic Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)
let a be F1 -algebraic Element of E1; :: thesis: for b being F2 -algebraic Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)
let b be F2 -algebraic Element of E2; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)
let p be irreducible Element of the carrier of (Polynom-Ring F1); :: thesis: ( Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 implies (PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2) )
assume AS: ( Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 ) ; :: thesis: (PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)
hence MinPoly (b,F2) = NormPolynomial ((PolyHom h) . p) by uu4
.= (PolyHom h) . (NormPolynomial p) by uu5
.= (PolyHom h) . (MinPoly (a,F1)) by AS, uu4 ;
:: thesis: verum