:: Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials
::  by Christoph Schwarzweller
:: 
:: Received October 25, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, ALGSEQ_1, VECTSP_2,
      STRUCT_0, SUBSET_1, SUPINF_2, BINOP_1, NAT_1, MESFUNC1, REALSET1, C0SP1,
      FUNCT_4, FUNCT_2, POLYNOM1, POLYNOM2, POLYNOM3, FUNCSDOM, RLVECT_5,
      PARTFUN1, EC_PF_1, HURWITZ, RLVECT_1, RLVECT_2, FINSEQ_1, CARD_FIL,
      FUNCT_1, RELAT_1, LATTICES, CARD_1, IDEAL_1, GCD_1, GROUP_6, XBOOLE_0,
      FINSET_1, NUMBERS, MSSUBFAM, POLYNOM5, GROUP_1, ZFMISC_1, FUNCT_7,
      POLYNOM4, AFINSQ_1, GROUP_4, INT_1, VECTSP10, CAT_1, FDIFF_1, YELLOW_8,
      RATFUNC1, RING_2, RING_3, ALGNUM_1, ARYTM_1, RLVECT_3, FIELD_4, NEWTON,
      WELLORD1, XXREAL_0, CARD_3, FUNCOP_1, XCMPLX_0, FOMODEL1, FIELD_1,
      RLSUB_1, FIELD_6;
 notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, ORDINAL1, REALSET1,
      PARTFUN1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, ZFMISC_1, NUMBERS,
      FINSET_1, CARD_1, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, FUNCT_4, FUNCT_7,
      IDEAL_1, STRUCT_0, GCD_1, VFUNCT_1, POLYNOM1, POLYNOM3, POLYNOM4,
      POLYNOM5, GROUP_1, GROUP_6, VECTSP10, VECTSP_4, VECTSP_6, VECTSP_7,
      BINOM, ALGSTR_0, RLVECT_1, VECTSP_2, VECTSP_9, MATRLIN, HURWITZ,
      VECTSP_1, ALGSEQ_1, C0SP1, EC_PF_1, RATFUNC1, RING_1, RING_2, RING_3,
      RING_4, ALGNUM_1, FIELD_1, FIELD_4, FIELD_5;
 constructors FUNCT_4, POLYNOM4, FUNCT_7, NAT_D, VFUNCT_1, RATFUNC1, GCD_1,
      REALSET1, BINOM, RINGCAT1, ALGSEQ_1, VECTSP_9, POLYDIFF, ALGNUM_1,
      VECTSP_6, FIELD_4, FIELD_5;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XCMPLX_0, XXREAL_0,
      XREAL_0, NAT_1, INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, EC_PF_1,
      POLYNOM4, FUNCT_2, ALGSTR_0, POLYNOM3, SUBSET_1, MOD_4, RLVECT_1,
      FINSET_1, FUNCT_1, VFUNCT_1, CARD_1, C0SP1, RATFUNC1, RELAT_1, RINGCAT1,
      RING_1, RING_2, RING_3, RING_4, RING_5, POLYDIFF, REALSET1, POLYNOM5,
      FIELD_4, FIELD_5;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;


begin :: Preliminaries

theorem :: FIELD_6:1
for R being Ring holds R is degenerated iff the carrier of R = {0.R};

registration
let F be Field;
cluster {0.F}-Ideal -> maximal;
end;

registration
let R be non degenerated non almost_left_invertible comRing;
cluster {0.R}-Ideal -> non maximal;
end;

definition
let R be Ring;
attr R is field-containing means
:: FIELD_6:def 1
  ex F being Field st F is Subring of R;
end;

registration
cluster field-containing for Ring;
end;

definition
let R be field-containing Ring;
mode Subfield of R -> Field means
:: FIELD_6:def 2
  it is Subring of R;
end;

theorem :: FIELD_6:2
for R being non degenerated Ring
for p being non zero Polynomial of R holds p.(deg p) = LC p;

registration
let R be non degenerated Ring;
let p be non zero Polynomial of R;
cluster LM p -> non zero;
end;

theorem :: FIELD_6:3
for R being Ring, p being Polynomial of R holds deg(LM p) = deg p;

theorem :: FIELD_6:4
for R being Ring, p being Polynomial of R holds LC (LM p) = LC p;

theorem :: FIELD_6:5
for R being non degenerated Ring
for p being non zero Polynomial of R holds deg(p - LM p) < deg p;

theorem :: FIELD_6:6
for R being Ring
for p being Polynomial of R
for i being Nat holds (<%0.R,1.R%> *' p).(i+1) = p.i;

theorem :: FIELD_6:7
for R being Ring
for p being Polynomial of R holds (<%0.R,1.R%> *' p).0 = 0.R;

theorem :: FIELD_6:8
for R being domRing
for p being non zero Polynomial of R holds deg(<%0.R,1.R%> *' p) = deg(p) + 1;

theorem :: FIELD_6:9
for R being comRing,
    p being Polynomial of R
for a being Element of R holds eval(<%0.R,1.R%> *' p,a) = a * eval(p,a);

theorem :: FIELD_6:10
for R being Ring,
    S being RingExtension of R
for p being Element of the carrier of Polynom-Ring R,
    a being Element of R,
    b being Element of S st b = a holds Ext_eval(p,b) = eval(p,a);

theorem :: FIELD_6:11
for F being Field,
    p being Element of the carrier of Polynom-Ring F
for E being FieldExtension of F,
    K being E-extending FieldExtension of F
for a being Element of E, b being Element of K st a = b
holds Ext_eval(p,a) = Ext_eval(p,b);

registration
let L be non empty ZeroStr,
    a,b be Element of L;
let f be (the carrier of L)-valued Function;
let x,y be object;
cluster f +* (x,y) --> (a,b) -> (the carrier of L)-valued;
end;

registration
let L be non empty ZeroStr,
    a,b be Element of L;
let f be finite-Support sequence of L;
let x,y be object;
cluster f +* (x,y) --> (a,b) -> finite-Support for sequence of L;
end;


begin :: On Subrings and Subfields

theorem :: FIELD_6:12
for R1,R2 being strict Ring
st R1 is Subring of R2 & R2 is Subring of R1 holds R1 = R2;

theorem :: FIELD_6:13
for S being Ring,
    R1,R2 being Subring of S
holds R1 is Subring of R2 iff the carrier of R1 c= the carrier of R2;

theorem :: FIELD_6:14
for S being Ring,
    R1,R2 being strict Subring of S
holds R1 = R2 iff the carrier of R1 = the carrier of R2;

theorem :: FIELD_6:15
for S being Ring,
    R being Subring of S
for x,y being Element of S,
    x1,y1 being Element of R st x = x1 & y = y1 holds x + y = x1 + y1;

theorem :: FIELD_6:16
for S being Ring,
    R being Subring of S
for x,y being Element of S,
    x1,y1 being Element of R st x = x1 & y = y1 holds x * y = x1 * y1;

theorem :: FIELD_6:17
for S being Ring,
    R being Subring of S
for x being Element of S, x1 being Element of R st x = x1 holds -x = -x1;

theorem :: FIELD_6:18
for E being Field,
    F being Subfield of E
for x being non zero Element of E,
    x1 being Element of F st x = x1 holds x" = x1";

theorem :: FIELD_6:19
for S being Ring,
    R being Subring of S
for x being Element of S, x1 being Element of R
for n being Element of NAT st x = x1 holds x|^n = x1|^n;

theorem :: FIELD_6:20
for S being Ring,
    R being Subring of S
for x1,x2 being Element of S, y1,y2 being Element of R
st x1 = y1 & x2 = y2 holds <%x1,x2%> = <%y1,y2%>;

theorem :: FIELD_6:21
for R being comRing,
    S being comRingExtension of R
for x1,x2 being Element of S, y1,y2 being Element of R
for n being Element of NAT
st x1 = y1 & x2 = y2 holds <%x1,x2%>`^n = <%y1,y2%>`^n;

theorem :: FIELD_6:22
for R being domRing,
    S being domRingExtension of R
for n being non zero Element of NAT
for a being Element of S holds Ext_eval(<%0.R,1.R%>`^n,a) = a|^n;

theorem :: FIELD_6:23
for R being Ring,
    S being RingExtension of R
for a being Element of R, b being Element of S st a = b holds a|R = b|S;

theorem :: FIELD_6:24
for F being Field,
    E being FieldExtension of F
for p being Element of the carrier of Polynom-Ring F
for q being Element of the carrier of Polynom-Ring E st p = q
holds NormPolynomial p = NormPolynomial q;

theorem :: FIELD_6:25
for F being Field,
    E being FieldExtension of F
for p being Element of the carrier of Polynom-Ring F
for a being Element of E
holds Ext_eval(p,a) = 0.E iff Ext_eval(NormPolynomial p,a) = 0.E;

theorem :: FIELD_6:26
for R being Ring,
    S being RingExtension of R
for a being Element of S,
    p being Polynomial of R holds Ext_eval(-p,a) = - Ext_eval(p,a);

theorem :: FIELD_6:27
for R being Ring,
    S being RingExtension of R
for a being Element of S,
    p,q being Polynomial of R
holds Ext_eval(p-q,a) = Ext_eval(p,a) - Ext_eval(q,a);

theorem :: FIELD_6:28
for R being Ring,
    S being RingExtension of R
for a being Element of S,
    p being constant Polynomial of R holds Ext_eval(p,a) = LC p;

theorem :: FIELD_6:29
for R being non degenerated Ring,
    S being RingExtension of R
for a,b being Element of S,
    p being non zero Polynomial of R st b = LC p holds
Ext_eval(Leading-Monomial p,a) = b * a|^(deg p);


begin :: Ring and Field Adjunctions

definition
let R be Ring,
    S be RingExtension of R;
let T be Subset of S;
func carrierRA(T) -> non empty Subset of S equals
:: FIELD_6:def 3
  {x where x is Element of S :
      for U being Subring of S
               st R is Subring of U & T is Subset of U holds x in U};
end;

definition
let R be Ring,
    S be RingExtension of R;
let T be Subset of S;
func RingAdjunction(R,T) -> strict doubleLoopStr means
:: FIELD_6:def 4
  the carrier of it = carrierRA(T) &
  the addF of it = (the addF of S)||carrierRA(T) &
  the multF of it = (the multF of S)||carrierRA(T) &
  the OneF of it = 1.S &
  the ZeroF of it = 0.S;
end;

notation
let R be Ring,
    S be RingExtension of R;
let T be Subset of S;
synonym RAdj(R,T) for RingAdjunction(R,T);
end;

registration
let R be Ring,
    S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> non empty;
end;

registration
let R be non degenerated Ring,
    S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> non degenerated;
end;

registration
let R be Ring,
    S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> Abelian add-associative right_zeroed right_complementable;
end;

registration
let R be comRing,
    S be comRingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> commutative;
end;

registration
let R be Ring,
    S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> associative well-unital distributive;
end;

theorem :: FIELD_6:30
for R being Ring,
    S being RingExtension of R
for T being Subset of S holds T is Subset of RAdj(R,T);

theorem :: FIELD_6:31
for R being Ring,
    S being RingExtension of R
for T being Subset of S holds R is Subring of RAdj(R,T);

theorem :: FIELD_6:32
for R being Ring,
    S being RingExtension of R,
    T being Subset of S
for U being Subring of S st R is Subring of U & T is Subset of U
holds RAdj(R,T) is Subring of U;

theorem :: FIELD_6:33
for R being strict Ring,
    S being RingExtension of R,
    T being Subset of S holds RAdj(R,T) = R iff T is Subset of R;

definition
let R be Ring,
    S be RingExtension of R;
let T be Subset of S;
redefine func RAdj(R,T) -> strict Subring of S;
end;

registration
let R be Ring,
    S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> R-extending;
end;

registration
let F be Field,
    R be RingExtension of F;
let T be Subset of R;
cluster RAdj(F,T) -> field-containing;
end;

theorem :: FIELD_6:34
for F being Field,
    R being RingExtension of F
for T being Subset of R holds F is Subfield of RAdj(F,T);

definition
let F be Field,
    E be FieldExtension of F;
let T be Subset of E;
func carrierFA(T) -> non empty Subset of E equals
:: FIELD_6:def 5
  {x where x is Element of E :
      for U being Subfield of E
               st F is Subfield of U & T is Subset of U holds x in U};
end;

definition
let F be Field,
    E be FieldExtension of F;
let T be Subset of E;
func FieldAdjunction(F,T) -> strict doubleLoopStr means
:: FIELD_6:def 6
  the carrier of it = carrierFA(T) &
  the addF of it = (the addF of E)||carrierFA(T) &
  the multF of it = (the multF of E)||carrierFA(T) &
  the OneF of it = 1.E &
  the ZeroF of it = 0.E;
end;

notation
let F be Field,
    E be FieldExtension of F;
let T be Subset of E;
synonym FAdj(F,T) for FieldAdjunction(F,T);
end;

registration
let F be Field,
    E be FieldExtension of F;
let T be Subset of E;
cluster FAdj(F,T) -> non degenerated;
end;

registration
let F be Field,
    E be FieldExtension of F;
let T be Subset of E;
cluster FAdj(F,T) -> Abelian add-associative right_zeroed right_complementable;
end;

registration
let F be Field,
    E be FieldExtension of F;
let T be Subset of E;
cluster FieldAdjunction(F,T) -> commutative associative well-unital
                                distributive almost_left_invertible;
end;

theorem :: FIELD_6:35
for F being Field,
    E being FieldExtension of F
for T being Subset of E holds T is Subset of FAdj(F,T);

theorem :: FIELD_6:36
for F being Field,
    E being FieldExtension of F
for T being Subset of E holds F is Subfield of FAdj(F,T);

theorem :: FIELD_6:37
for F being Field,
    E being FieldExtension of F,
    T being Subset of E
for U being Subfield of E st F is Subfield of U & T is Subset of U
holds FAdj(F,T) is Subfield of U;

theorem :: FIELD_6:38
for F being strict Field,
    E being FieldExtension of F,
    T being Subset of E holds FAdj(F,T) = F iff T is Subset of F;

definition
let F be Field,
    E be FieldExtension of F;
let T be Subset of E;
redefine func FAdj(F,T) -> strict Subfield of E;
end;

registration
let F be Field,
    E be FieldExtension of F;
let T be Subset of E;
cluster FAdj(F,T) -> F-extending;
end;

theorem :: FIELD_6:39
for F being Field,
    E being FieldExtension of F,
    T being Subset of E holds RAdj(F,T) is Subring of FAdj(F,T);

theorem :: FIELD_6:40
for F being Field,
    E being FieldExtension of F,
    T being Subset of E holds RAdj(F,T) = FAdj(F,T) iff RAdj(F,T) is Field;


begin :: Algebraic Elements

registration
let R be non degenerated comRing,
    S be comRingExtension of R;
let a be Element of S;
cluster hom_Ext_eval(a,R) -> additive multiplicative unity-preserving;
end;

registration
let R be non degenerated comRing;
cluster -> (Polynom-Ring R)-homomorphic for comRingExtension of R;
end;

registration
let F be Field;
cluster (Polynom-Ring F)-homomorphic for FieldExtension of F;
end;

definition
let F be Field,
    E be FieldExtension of F;
let a be Element of E;
attr a is F-algebraic means
:: FIELD_6:def 7
  ker(hom_Ext_eval(a,F)) <> {0.(Polynom-Ring F)};
end;

notation
let F be Field,
    E be FieldExtension of F;
let a be Element of E;
antonym a is F-transcendental for a is F-algebraic;
end;

theorem :: FIELD_6:41
for R being Ring,
    S being RingExtension of R
for a being Element of S holds Ann_Poly(a,R) = ker(hom_Ext_eval(a,R));

theorem :: FIELD_6:42
for F being Field,
    E being FieldExtension of F
for a being Element of E holds a is F-algebraic iff a is_integral_over F;

theorem :: FIELD_6:43
for F being Field,
    E being FieldExtension of F
for a being Element of E
holds a is F-algebraic iff
      ex p being non zero Polynomial of F st Ext_eval(p,a) = 0.E;

registration
let F be Field,
    E be FieldExtension of F;
cluster F-algebraic for Element of E;
end;

theorem :: FIELD_6:44
for F being Field,
    E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being Element of E holds RAdj(F,{a}) = Image hom_Ext_eval(a,F);

theorem :: FIELD_6:45
for F being Field,
    E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being Element of E
holds the carrier of RAdj(F,{a})
    = the set of all Ext_eval(p,a) where p is Polynomial of F;


begin

theorem :: FIELD_6:46
for F being Field
for V being VectSp of F, W being Subspace of V
for l1 being Linear_Combination of W
ex l2 being Linear_Combination of V
st Carrier l2 = Carrier l1 &
   for v being Element of V st v in Carrier l2 holds l2.v = l1.v;

theorem :: FIELD_6:47
for F being Field,
    E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp(E,F)
ex p being Polynomial of F
st deg p <= n &
   for i being Element of NAT st i <= n holds p.i = l.(a|^i);

theorem :: FIELD_6:48
for F being Field,
    E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp(E,F),
    p being non zero Polynomial of F
st l.(a|^(deg p)) = LC p & Carrier l = {a|^(deg p)}
holds Sum l = Ext_eval(LM p,a);

theorem :: FIELD_6:49
for F being Field,
    E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for M being Subset of VecSp(E,F)
   st M = {a|^i where i is Element of NAT : i <= n} &
      for i,j being Element of NAT st i < j & j <= n holds a|^i <> a|^j
for l being Linear_Combination of M
for p being Polynomial of F
st deg p <= n &
   for i being Element of NAT st i <= n holds p.i = l.(a|^i)
holds Ext_eval(p,a) = Sum l;


begin :: Minimal Polynomials

notation
let F be Field,
    E be FieldExtension of F;
let a be F-algebraic Element of E;
synonym MinPoly(a,F) for minimal_polynom(a,F);
end;

registration
let F be Field,
    E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster MinPoly(a,F) -> monic irreducible;
end;

theorem :: FIELD_6:50
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E,
    p being Element of the carrier of Polynom-Ring F
holds p = MinPoly(a,F) iff
      (p is monic & p is irreducible & ker(hom_Ext_eval(a,F)) = {p}-Ideal);

theorem :: FIELD_6:51
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E,
    p being Element of the carrier of Polynom-Ring F
holds p = MinPoly(a,F) iff
      (p is monic & Ext_eval(p,a) = 0.E &
       for q being non zero Polynomial of F
                         st Ext_eval(q,a) = 0.E holds deg p <= deg q);

theorem :: FIELD_6:52
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E,
    p being Element of the carrier of Polynom-Ring F
holds p = MinPoly(a,F) iff
      (p is monic & p is irreducible & Ext_eval(p,a) = 0.E);

theorem :: FIELD_6:53
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E,
    p being Element of the carrier of Polynom-Ring F
holds Ext_eval(p,a) = 0.E iff MinPoly(a,F) divides p;

theorem :: FIELD_6:54
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E
holds MinPoly(a,F) = rpoly(1,a) iff a in the carrier of F;

theorem :: FIELD_6:55
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E
for i,j being Element of NAT st i < j & j < deg MinPoly(a,F) holds a|^i <> a|^j
;

theorem :: FIELD_6:56
for F being Field,
    E being (Polynom-Ring F)-homomorphic FieldExtension of F,
    a being Element of E holds a is F-algebraic iff FAdj(F,{a}) = RAdj(F,{a});

theorem :: FIELD_6:57
for F being Field,
    E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being non zero Element of E holds a is F-algebraic iff a" in RAdj(F,{a});

theorem :: FIELD_6:58
for F being Field,
    E being FieldExtension of F
for a being Element of E
holds a is F-transcendental iff RAdj(F,{a}),Polynom-Ring F are_isomorphic;

theorem :: FIELD_6:59
for F being Field,
    E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being F-algebraic Element of E
holds (Polynom-Ring F)/({MinPoly(a,F)}-Ideal), FAdj(F,{a}) are_isomorphic;


begin ::  The Basis of Vector Space F(a)

definition
let F be Field,
    E be FieldExtension of F;
let a be F-algebraic Element of E;
func Base a -> non empty Subset of VecSp(FAdj(F,{a}),F) equals
:: FIELD_6:def 8
  { a|^n where n is Element of NAT : n < deg MinPoly(a,F) };
end;

registration
let F be Field,
    E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster Base a -> finite;
end;

theorem :: FIELD_6:60
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E
for p being Polynomial of F holds Ext_eval(p,a) in Lin(Base a);

theorem :: FIELD_6:61
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E
for l being Linear_Combination of Base a
ex p being Polynomial of F
st deg p < deg MinPoly(a,F) &
   for i being Element of NAT st i < deg MinPoly(a,F) holds p.i = l.(a|^i);

theorem :: FIELD_6:62
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E
for l being Linear_Combination of Base a,
    p being non zero Polynomial of F
st l.(a|^(deg p)) = LC p & Carrier l = {a|^(deg p)}
holds Sum l = Ext_eval(LM p,a);

theorem :: FIELD_6:63
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E
for l being Linear_Combination of Base a
for p being Polynomial of F
st deg p < deg MinPoly(a,F) &
   for i being Element of NAT st i < deg MinPoly(a,F) holds p.i = l.(a|^i)
holds Sum l = Ext_eval(p,a);

theorem :: FIELD_6:64
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E
for l being Linear_Combination of Base a
holds Sum(l) = 0.F implies l = ZeroLC VecSp(FAdj(F,{a}),F);

theorem :: FIELD_6:65
for F being Field,
    E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being F-algebraic Element of E holds
Base a is Basis of VecSp(FAdj(F,{a}),F);

theorem :: FIELD_6:66
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E holds card(Base a) = deg MinPoly(a,F);

theorem :: FIELD_6:67
for F being Field,
    E being FieldExtension of F
for a being F-algebraic Element of E
holds deg(FAdj(F,{a}),F) = deg MinPoly(a,F);

registration
let F be Field,
    E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster FAdj(F,{a}) -> F-finite;
end;

theorem :: FIELD_6:68
for F being Field,
    E being FieldExtension of F
for a being Element of E
holds a is F-algebraic iff FAdj(F,{a}) is F-finite;