:: On Roots of Polynomials and Algebraically Closed Fields
:: by Christoph Schwarzweller
::
:: Received August 30, 2017
:: Copyright (c) 2017 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);