:: On Roots of Polynomials and Algebraically Closed Fields
::  by Christoph Schwarzweller
:: 
:: Received August 30, 2017
:: Copyright (c) 2017-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, POLYNOM2, POLYNOM1, ARYTM_1, FUNCT_1, ABIAN, POLYNOM3,
      RELAT_1, FINSEQ_1, AFINSQ_1, VECTSP_1, INT_1, INT_2, ALGSEQ_1, TARSKI,
      FUNCT_4, ALGSTR_0, POLYNOM5, PARTFUN1, HURWITZ, ORDINAL1, UPROOTS,
      PRE_POLY, SGRAPH1, XCMPLX_0, VECTSP_2, FUNCSDOM, STRUCT_0, SUBSET_1,
      SUPINF_2, NAT_1, NUMBERS, CARD_1, MESFUNC1, XXREAL_0, RATFUNC1, XXREAL_2,
      GROUP_1, FINSET_1, ZFMISC_1, XBOOLE_0, ORDINAL4, NEWTON, CARD_3,
      VALUED_0, CAT_1, FUNCOP_1, RING_3, RING_5;
 notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, FUNCT_4, XCMPLX_0, FINSET_1,
      CARD_1, XXREAL_0, XXREAL_2, NAT_D, GROUP_4, RELAT_1, RELSET_1, VECTSP_2,
      ORDINAL1, NUMBERS, VECTSP_1, FUNCT_1, PARTFUN1, NAT_1, INT_1, INT_2,
      RLVECT_1, FINSEQ_1, POLYNOM1, ALGSEQ_1, RVSUM_1, RECDEF_1, ABIAN,
      GROUP_1, BINOM, FUNCT_7, ALGSTR_0, STRUCT_0, PRE_POLY, TERMORD, POLYNOM3,
      POLYNOM4, POLYNOM5, HURWITZ, RATFUNC1, UPROOTS, RING_2, RING_3, RING_4;
 constructors BINOM, RECDEF_1, POLYNOM4, ALGSEQ_1, HURWITZ, FUNCT_4, WSIERP_1,
      FVSUM_1, RELSET_1, ABIAN, NAT_D, GROUP_4, RATFUNC1, RING_3, RING_4,
      BINOP_2, XXREAL_2, TERMORD;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0,
      NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1, NAT_6, ALGSTR_1,
      POLYNOM3, POLYNOM4, POLYNOM5, VALUED_0, FUNCT_1, POLYNOM1, ABIAN,
      XXREAL_2, PRE_POLY, SUBSET_1, RLVECT_1, FINSET_1, CARD_1, RATFUNC1,
      UPROOTS, HURWITZ2, PBOOLE, RING_3, RING_4, EC_PF_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve n for Nat;

registration
 cluster non trivial non prime for Nat;
end;

theorem :: RING_5:1
for n being even Nat,
    x being Element of F_Real holds x|^n >= 0.F_Real;

theorem :: RING_5:2
for R being Ring, a being Element of R holds 2 '*' a = a + a;

theorem :: RING_5:3
for R being Ring, a being Element of R holds a |^ 2 = a * a;

registration
let F be Field;
let a be Element of F;
reduce a / 1.F to a;
end;

registration
cluster Z/2 -> non trivial almost_left_invertible;
end;

registration
let n be non trivial non prime Nat;
cluster Z/n -> non domRing-like;
end;

registration
cluster Z/6 -> non degenerated;
end;

begin :: Some More Properties of Polynomials

registration
let R be non degenerated Ring;
cluster -> non-zero for non zero Polynomial of R;
cluster monic -> non zero for Polynomial of R;
end;

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

registration
let R be Ring;
let p be zero Polynomial of R;
let q be Polynomial of R;
cluster p *' q -> zero;
cluster q *' p -> zero;
end;

registration
let R be Ring;
let p be zero Polynomial of R;
let q be Polynomial of R;
reduce p + q to q;
reduce q + p to q;
end;

registration
let R be Ring;
let p be Polynomial of R;
reduce p *' 0_.(R) to 0_.(R);
reduce p *' 1_.(R) to p;
reduce (0_.(R)) *' p to 0_.(R);
reduce (1_.(R)) *' p to p;
end;

registration
let R be Ring;
let p be Polynomial of R;
reduce 1.R * p to p;
end;

theorem :: RING_5:4
for R being domRing,
    p being Polynomial of R
for a being non zero Element of R holds deg(a*p) = deg p;

theorem :: RING_5:5
for R being domRing,
    p being Polynomial of R
for a being Element of R holds LC(a * p) = a * LC(p);

theorem :: RING_5:6
for R being domRing, a being Element of R holds LC(a|R) = a;

theorem :: RING_5:7
for R being domRing,
    p being Polynomial of R
for v,x being Element of R holds eval(v*p,x) = v * eval(p,x);

theorem :: RING_5:8
for R being Ring, a,b being Element of R holds eval(a|R,b) = a;

registration
let R be domRing;
let p,q be monic Polynomial of R;
cluster p *' q -> monic;
end;

registration
let R be domRing;
let a be Element of R;
let k be Nat;
cluster rpoly(1,a)`^k -> non zero monic;
end;

theorem :: RING_5:9
for R being non degenerated Ring,
    a being Element of R,
    k being non zero Element of NAT holds LC rpoly(k,a) = 1.R;

theorem :: RING_5:10
for R being non degenerated well-unital non empty doubleLoopStr
for a being Element of R holds <%-a, 1.R%> = rpoly(1,a);

theorem :: RING_5:11
for R being domRing
for p being Polynomial of R
for x being Element of R holds eval(p,x) = 0.R iff rpoly(1,x) divides p;

theorem :: RING_5:12
for F being domRing,
    p,q being Polynomial of F
for a being Element of F
st rpoly(1,a) divides (p*'q) holds rpoly(1,a) divides p or rpoly(1,a) divides q
;

theorem :: RING_5:13
for R being domRing,
    p being Polynomial of R
for q being non zero Polynomial of R st p divides q holds deg p <= deg q;

theorem :: RING_5:14
for R being non degenerated comRing,
    q being Polynomial of R
for p being non zero Polynomial of R
for b being non zero Element of R st q divides p holds q divides (b*p);

theorem :: RING_5:15
for F being Field,
    q being Polynomial of F
for p being non zero Polynomial of F
for b being non zero Element of F holds q divides p iff q divides (b*p);

theorem :: RING_5:16
for R being domRing,
    p being non zero Polynomial of R
for a being Element of R,
    b being non zero Element of R
holds rpoly(1,a) divides p iff rpoly(1,a) divides (b * p);

theorem :: RING_5:17
for R being domRing,
    p being non zero Polynomial of R
for a being Element of R,
    b being non zero Element of R
holds rpoly(1,a)`^n divides p iff rpoly(1,a)`^n divides (b * p);

registration
let R be domRing;
let p be non zero Polynomial of R;
let b be non zero Element of R;
cluster b * p -> non zero;
end;


begin :: On Roots of Polynomials

registration
let R be non degenerated Ring;
cluster 1_.(R) -> non with_roots;
end;

registration
let R be non degenerated Ring;
let a be non zero Element of R;
cluster a|R -> non with_roots;
end;

registration
let R be non degenerated Ring;
cluster non zero with_roots -> non constant for Polynomial of R;
end;

registration
let R be non degenerated Ring;
cluster non with_roots -> non zero for Polynomial of R;
end;

registration
let R be non degenerated Ring;
let a be Element of R;
cluster rpoly(1,a) -> non zero with_roots;
end;

registration
let R be non degenerated Ring;
cluster non zero non with_roots for Polynomial of R;
cluster non zero with_roots for Polynomial of R;
end;

registration
let R be domRing;
let p be non with_roots Polynomial of R;
let a be non zero Element of R;
cluster a * p -> non with_roots;
end;

registration
let R be domRing;
let p be with_roots Polynomial of R;
let a be Element of R;
cluster a * p -> with_roots;
end;

registration
let R be non degenerated comRing;
let p be with_roots Polynomial of R;
let q be Polynomial of R;
cluster p *' q -> with_roots;
end;

registration
let R be domRing;
let p,q be non with_roots Polynomial of R;
cluster p *' q -> non with_roots;
end;

registration
let R be non degenerated comRing;
let a be Element of R;
let k be non zero Element of NAT;
cluster rpoly(k,a) -> non constant monic with_roots;
end;

registration
let R be non degenerated Ring;
cluster non constant monic for Polynomial of R;
end;

registration
let R be domRing;
let a be Element of R;
let k be non zero Nat;
let n be non zero Element of NAT;
cluster rpoly(n,a)`^k -> non constant monic with_roots;
end;

registration
let R be Ring;
let p be with_roots Polynomial of R;
cluster Roots(p) -> non empty;
end;

registration
let R be non degenerated Ring;
let p be non with_roots Polynomial of R;
cluster Roots(p) -> empty;
end;

registration
let R be domRing;
cluster monic with_roots for Polynomial of R;
cluster monic non with_roots for Polynomial of R;
end;

theorem :: RING_5:18
for R being non degenerated Ring,
    a being Element of R holds Roots rpoly(1,a) = {a};

theorem :: RING_5:19
for F being domRing,
    p being Polynomial of F
for b being non zero Element of F holds Roots(b * p) = Roots p;

theorem :: RING_5:20
ex p,q being Polynomial of Z/6 st not Roots(p*'q) c= Roots(p) \/ Roots(q);

theorem :: RING_5:21
for R being domRing,
    a,b being Element of R holds rpoly(1,a) divides rpoly(1,b) iff a = b;

theorem :: RING_5:22
for R being domRing,
    p being non zero Polynomial of R holds card(Roots p) <= deg p;


begin :: More about Bags

notation
let X be non empty set;
let B be bag of X;
synonym card B for Sum B;
end;

registration
let X be non empty set;
cluster zero for bag of X;
cluster non zero for bag of X;
end;

registration
let X be non empty set;
let b1 be bag of X;
let b2 be bag of X;
cluster b1 + b2 -> X-defined;
end;

registration
let X be non empty set;
let b1 be bag of X;
let b2 be bag of X;
cluster b1 + b2 -> total;
end;

theorem :: RING_5:23
for X being non empty set,
    b being bag of X holds card b = 0 iff support b = {};

theorem :: RING_5:24
for X being non empty set,
    b being bag of X holds b is zero iff support b = {};

theorem :: RING_5:25
for X being non empty set,
    b being bag of X holds b is zero iff rng b = {0};

registration
let X be non empty set;
let b1 be non zero bag of X;
let b2 be bag of X;
cluster b1 + b2 -> non zero;
end;

theorem :: RING_5:26
for X being non empty set,
    b being bag of X,
    x being Element of X holds support b = {x} implies b = ({x},b.x)-bag;

theorem :: RING_5:27
for X being non empty set,
    b being non empty bag of X,
    x being Element of X
holds support b = {x} iff (b = ({x},b.x)-bag & b.x <> 0);

definition
let X be set;
let S be finite Subset of X;
func Bag S -> bag of X equals
:: RING_5:def 1
  (S,1)-bag;
end;

registration
let X be non empty set;
let S be non empty finite Subset of X;
cluster Bag S -> non zero;
end;

definition
let X be non empty set;
let b be bag of X;
let a be Element of X;
func b \ a -> bag of X equals
:: RING_5:def 2
  b +* (a,0);
end;

theorem :: RING_5:28
for X being non empty set,
    b being bag of X,
    a being Element of X holds b \ a = b iff not a in support b;

theorem :: RING_5:29
for X being non empty set,
    b being bag of X,
    a being Element of X holds support(b \ a) = support b \ {a};

theorem :: RING_5:30
for X being non empty set,
    b being bag of X,
    a being Element of X holds (b \ a) + ({a},b.a)-bag = b;

theorem :: RING_5:31
for X being non empty set,
    a being Element of X,
    n being Element of NAT holds card(({a},n)-bag) = n;


begin :: On Multiple Roots of Polynomials

registration
let R be domRing;
let p be non zero with_roots Polynomial of R;
cluster BRoots p -> non zero;
end;

theorem :: RING_5:32
for R being non degenerated comRing,
    p being non zero Polynomial of R
for a being Element of R
holds multiplicity(p,a) = 0 iff not rpoly(1,a) divides p;

theorem :: RING_5:33
for R being domRing,
    p being non zero Polynomial of R
for a being Element of R
holds multiplicity(p,a) = n
      iff (rpoly(1,a)`^n divides p & not rpoly(1,a)`^(n+1) divides p);

theorem :: RING_5:34
for R being domRing,
    a being Element of R holds multiplicity(rpoly(1,a),a) = 1;

theorem :: RING_5:35
for R being domRing,
    a,b being Element of R st b <> a holds multiplicity(rpoly(1,a),b) = 0;

theorem :: RING_5:36
for R being domRing,
    p being non zero Polynomial of R
for b being non zero Element of R,
    a being Element of R holds multiplicity(p,a) = multiplicity(b*p,a);

theorem :: RING_5:37
for R being domRing,
    p being non zero Polynomial of R
for b being non zero Element of R holds BRoots(b * p) = BRoots p;

theorem :: RING_5:38
for R being domRing,
    p being non zero non with_roots Polynomial of R
holds BRoots p = EmptyBag(the carrier of R);

theorem :: RING_5:39
for R being domRing,
    a being non zero Element of R holds card BRoots a|R = 0;

theorem :: RING_5:40
for R being domRing,
    a being Element of R holds card BRoots rpoly(1,a) = 1;

theorem :: RING_5:41
for R being domRing,
    p,q being non zero Polynomial of R
holds card BRoots(p*'q) = card BRoots p + card BRoots q;

theorem :: RING_5:42
for R being domRing,
    p being non zero Polynomial of R holds card(BRoots p) <= deg p;


begin

definition
let R be unital non empty doubleLoopStr;
let n be Nat;
func npoly(R,n) -> sequence of R equals
:: RING_5:def 3
  0_.(R) +* (0,n) --> (1.R,1.R);
end;

registration
let R be unital non empty doubleLoopStr;
let n be Nat;
cluster npoly(R,n) -> finite-Support;
end;

registration
let R be unital non degenerated doubleLoopStr,
    n be Nat;
cluster npoly(R,n) -> non zero;
end;

theorem :: RING_5:43
for R being unital non degenerated doubleLoopStr holds deg npoly(R,n) = n;

theorem :: RING_5:44
for R being unital non degenerated doubleLoopStr holds LC npoly(R,n) = 1.R;

theorem :: RING_5:45
for R being non degenerated Ring,
    x being Element of R holds eval(npoly(R,0),x) = 1.R;

theorem :: RING_5:46
for R being non degenerated Ring,
    n being non zero Nat,
    x being Element of R holds eval(npoly(R,n),x) = x|^n + 1.R;

theorem :: RING_5:47
for n being even Nat,
    x being Element of F_Real holds eval(npoly(F_Real,n),x) > 0.F_Real;

theorem :: RING_5:48
for n being odd Nat
holds eval(npoly(F_Real,n),-1.F_Real) = 0.F_Real;

theorem :: RING_5:49
eval(npoly(Z/2,2),1.(Z/2)) = 0.(Z/2);

registration
let n be even Nat;
cluster npoly(F_Real,n) -> non with_roots;
end;

registration
let n be odd Nat;
cluster npoly(F_Real,n) -> with_roots;
end;

registration
cluster npoly(Z/2,2) -> with_roots;
end;


begin :: the polynomials (x-a1) * (x-a2) * ... * (x-an)

definition
let R be Ring;
mode Ppoly of R -> Polynomial of R means
:: RING_5:def 4
  ex F being non empty FinSequence of Polynom-Ring R
  st it = Product F &
     for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a);
end;

registration
let R be domRing;
cluster -> non constant monic with_roots for Ppoly of R;
end;

theorem :: RING_5:50
for R being domRing, p being Ppoly of R holds LC p = 1.R;

theorem :: RING_5:51
for R being domRing, a being Element of R holds rpoly(1,a) is Ppoly of R;

theorem :: RING_5:52
for R being domRing,
    p,q being Ppoly of R holds p *' q is Ppoly of R;

definition
let R be domRing;
let B be non zero bag of the carrier of R;
mode Ppoly of R,B -> Ppoly of R means
:: RING_5:def 5
  deg it = card B &
  for a being Element of R holds multiplicity(it,a) = B.a;
end;

theorem :: RING_5:53
for R being domRing,
    B being non zero bag of the carrier of R,
    p being Ppoly of R,B
for a being Element of R st a in support B holds eval(p,a) = 0.R;

theorem :: RING_5:54
for R being domRing,
    B being non zero bag of the carrier of R,
    p being Ppoly of R,B
for a being Element of R
holds rpoly(1,a) `^ (B.a) divides p & not rpoly(1,a) `^ (B.a + 1) divides p;

theorem :: RING_5:55
for R being domRing,
    B being non zero bag of the carrier of R,
    p being Ppoly of R,B holds BRoots(p) = B;

theorem :: RING_5:56
for R being domRing,
    B being non zero bag of the carrier of R
for p being Ppoly of R,B holds deg p = card BRoots p;

theorem :: RING_5:57
for R being domRing,
    a being Element of R holds rpoly(1,a) is Ppoly of R,Bag{a};

theorem :: RING_5:58
for R being domRing,
    B1,B2 being non zero bag of the carrier of R
for p being (Ppoly of R,B1),
    q being Ppoly of R,B2 holds p *' q is Ppoly of R,(B1+B2);

theorem :: RING_5:59
for R being domRing, p being Ppoly of R holds p is Ppoly of R,(BRoots p);

definition
let R be domRing;
let S be non empty finite Subset of R;
mode Ppoly of R,S is Ppoly of R,Bag S;
end;

theorem :: RING_5:60
for R being domRing,
    S being non empty finite Subset of R
for p being Ppoly of R,S holds deg p = card S;

theorem :: RING_5:61
for R being domRing,
    S being non empty finite Subset of R
for p being Ppoly of R,S
for a being Element of R st a in S
holds rpoly(1,a) divides p & not rpoly(1,a)`^2 divides p;

theorem :: RING_5:62
for R being domRing,
    S being non empty finite Subset of R,
    p being Ppoly of R,S
for a being Element of R st a in S holds eval(p,a) = 0.R;

theorem :: RING_5:63
for R being domRing,
    S being non empty finite Subset of R,
    p being Ppoly of R,S
holds Roots(p) = S;


begin :: Main Theorems

theorem :: RING_5:64
for R being domRing,
    p being non zero with_roots Polynomial of R
ex q being (Ppoly of R,BRoots p),
   r being non with_roots Polynomial of R st p = q *' r & Roots q = Roots p;

theorem :: RING_5:65
for R being domRing,
    p being non zero Polynomial of R holds card(Roots p) <= card(BRoots p);

theorem :: RING_5:66
for R being domRing,
    p being non constant Polynomial of R
holds card(BRoots p) = deg p iff
      ex a being Element of R, q being Ppoly of R st p = a * q;

theorem :: RING_5:67
for R being domRing,
    p,q being Polynomial of R
st (ex S being Subset of R
    st card S = max(deg p,deg q) + 1 &
       for a being Element of R st a in S holds eval(p,a) = eval(q,a))
holds p = q;

registration
let F be algebraic-closed Field;
cluster -> with_roots for non constant Polynomial of F;
end;

registration
cluster F_Real -> non algebraic-closed;
end;

registration
cluster -> non algebraic-closed for finite domRing;
end;

registration
cluster algebraic-closed -> almost_right_invertible for Ring;
end;

theorem :: RING_5:68
for F being algebraic-closed Field,
    p being non constant Polynomial of F
ex a being Element of F, q being Ppoly of F,(BRoots p) st a * q = p;

theorem :: RING_5:69
for F being algebraic-closed Field,
    p being non constant monic Polynomial of F holds p is Ppoly of F,BRoots p;

theorem :: RING_5:70
for F being Field
holds F is algebraic-closed iff
      (for p being non constant monic Polynomial of F holds p is Ppoly of F);