:: The Ring of Polynomials :: by Robert Milewski :: :: Received April 17, 2000 :: Copyright (c) 2000-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 NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, FINSEQ_1, STRUCT_0, SUBSET_1, RELAT_1, FUNCT_1, SUPINF_2, CARD_3, NAT_1, PARTFUN1, FINSEQ_5, ORDINAL4, ARYTM_3, XXREAL_0, FINSEQ_3, FINSEQ_2, PRE_POLY, TARSKI, CARD_1, ORDERS_1, RELAT_2, FINSET_1, ARYTM_1, FUNCT_2, POLYNOM1, ALGSEQ_1, FUNCOP_1, FUNCT_4, MESFUNC1, LATTICES, VECTSP_1, BINOP_1, CLASSES1, GROUP_1, ZFMISC_1, POLYNOM3, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, RELAT_2, FUNCT_1, ORDERS_1, XXREAL_0, XREAL_0, NAT_1, NAT_D, CLASSES1, RELSET_1, PARTFUN1, FINSET_1, FUNCT_2, FUNCOP_1, FINSEQ_1, PRE_POLY, FINSEQ_2, FINSEQ_5, BINOP_1, RVSUM_1, FUNCT_7, TREES_4, VALUED_0, WSIERP_1, MATRIX_0, STRUCT_0, ALGSTR_0, MATRLIN, GROUP_1, RLVECT_1, VFUNCT_1, FVSUM_1, VECTSP_1, NORMSP_1, POLYNOM1, ALGSEQ_1, RECDEF_1; constructors BINOP_1, FINSEQOP, REALSET1, NAT_D, FINSEQ_5, WSIERP_1, ALGSEQ_1, TRIANG_1, POLYNOM1, RECDEF_1, BINARITH, CLASSES1, RELSET_1, FUNCT_7, MATRLIN, FVSUM_1, VFUNCT_1, NUMBERS; registrations ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, FINSEQ_5, STRUCT_0, VECTSP_1, VALUED_0, FINSET_1, RELSET_1, PRE_POLY, VFUNCT_1, CARD_1, FUNCT_1, FINSEQ_3; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin :: Preliminaries theorem :: POLYNOM3:1 for L be add-associative right_zeroed right_complementable non empty addLoopStr for p be FinSequence of the carrier of L st for i be Element of NAT st i in dom p holds p.i = 0.L holds Sum p = 0.L; theorem :: POLYNOM3:2 for V be Abelian add-associative right_zeroed non empty addLoopStr for p be FinSequence of the carrier of V holds Sum p = Sum Rev p; theorem :: POLYNOM3:3 for p be FinSequence of REAL holds Sum p = Sum Rev p; theorem :: POLYNOM3:4 for p be FinSequence of NAT for i be Element of NAT st i in dom p holds Sum p >= p.i; definition let D be non empty set; let i be Element of NAT; let p be FinSequence of D; redefine func Del(p,i) -> FinSequence of D; end; definition let D be non empty set; let a,b be Element of D; redefine func <*a,b*> -> Element of 2-tuples_on D; end; definition let D be non empty set; let k,n be Element of NAT; let p be Element of k-tuples_on D; let q be Element of n-tuples_on D; redefine func p^q -> Element of (k+n)-tuples_on D; end; definition let D be non empty set; let k,n be Nat; let p be FinSequence of k-tuples_on D; let q be FinSequence of n-tuples_on D; redefine func p ^^ q -> Element of ((k+n)-tuples_on D)*; end; scheme :: POLYNOM3:sch 1 SeqOfSeqLambdaD{D()->non empty set,A()->Element of NAT, T(Nat)-> Element of NAT, F(set,set)->Element of D()}: ex p be FinSequence of D()* st len p = A() & for k be Element of NAT st k in Seg A() holds len (p/.k) = T(k) & for n be Element of NAT st n in dom (p/.k) holds (p/.k).n = F(k,n); begin :: The Lexicographic Order of Finite Sequences definition let n be Nat; let p,q be Element of n-tuples_on NAT; pred p < q means :: POLYNOM3:def 1 ex i be Element of NAT st i in Seg n & p.i < q.i & for k be Nat st 1 <= k & k < i holds p.k = q.k; asymmetry; end; notation let n be Element of NAT; let p,q be Element of n-tuples_on NAT; synonym q > p for p < q; end; definition let n be Element of NAT; let p,q be Element of n-tuples_on NAT; pred p <= q means :: POLYNOM3:def 2 p < q or p = q; reflexivity; end; notation let n be Element of NAT; let p,q be Element of n-tuples_on NAT; synonym q >= p for p <= q; end; theorem :: POLYNOM3:5 for n be Element of NAT for p,q,r be Element of n-tuples_on NAT holds (p < q & q < r implies p < r) & ( p < q & q <= r or p <= q & q < r or p <= q & q <= r implies p <= r); theorem :: POLYNOM3:6 for n be Nat for p,q be Element of n-tuples_on NAT holds p <> q implies ex i be Element of NAT st i in Seg n & p.i <> q.i & for k be Nat st 1 <= k & k < i holds p.k = q.k; theorem :: POLYNOM3:7 for n be Element of NAT for p,q be Element of n-tuples_on NAT holds p <= q or p > q; definition let n be Element of NAT; func TuplesOrder n -> Order of n-tuples_on NAT means :: POLYNOM3:def 3 for p,q be Element of n-tuples_on NAT holds [p,q] in it iff p <= q; end; registration let n be Element of NAT; cluster TuplesOrder n -> being_linear-order; end; begin :: Decomposition of Natural Numbers definition let i be non zero Element of NAT; let n be Element of NAT; func Decomp(n,i) -> FinSequence of i-tuples_on NAT means :: POLYNOM3:def 4 ex A be finite Subset of i-tuples_on NAT st it = SgmX (TuplesOrder i,A) & for p be Element of i-tuples_on NAT holds p in A iff Sum p = n; end; registration let i be non zero Element of NAT; let n be Element of NAT; cluster Decomp(n,i) -> non empty one-to-one FinSequence-yielding; end; theorem :: POLYNOM3:8 for n be Element of NAT holds len Decomp(n,1) = 1; theorem :: POLYNOM3:9 for n be Element of NAT holds len Decomp(n,2) = n+1; theorem :: POLYNOM3:10 for n be Element of NAT holds Decomp(n,1) = <*<*n*>*>; theorem :: POLYNOM3:11 for i,j,n,k1,k2 be Element of NAT st Decomp(n,2).i = <*k1,n-'k1 *> & Decomp(n,2).j = <*k2,n-'k2*> holds i & Decomp(n,2).(i+1) = <*k2,n-'k2*> holds k2=k1+1; theorem :: POLYNOM3:13 for n be Element of NAT holds Decomp(n,2).1 = <*0,n*>; theorem :: POLYNOM3:14 for n,i be Element of NAT st i in Seg (n+1) holds Decomp(n,2).i = <*i-'1,n+1-'i*>; definition let L be non empty multMagma; let p,q,r be sequence of L; let t be FinSequence of 3-tuples_on NAT; func prodTuples(p,q,r,t) -> Element of (the carrier of L)* means :: POLYNOM3:def 5 len it = len t & for k be Element of NAT st k in dom t holds it.k = (p.((t/.k)/.1)) *(q.((t/.k)/.2))*(r.((t/.k)/.3)); end; theorem :: POLYNOM3:15 for L be non empty multMagma for p,q,r be sequence of L for t be FinSequence of 3-tuples_on NAT for P be Permutation of dom t for t1 be FinSequence of 3-tuples_on NAT st t1 = t*P holds prodTuples(p,q,r,t1) = prodTuples(p,q,r,t)*P; theorem :: POLYNOM3:16 for D be set, f be FinSequence of D*, i be Nat holds Card (f|i) = (Card f)|i; ::$CT theorem :: POLYNOM3:18 for p be FinSequence of NAT for i,j be Nat st i <= j holds Sum (p|i) <= Sum (p|j); ::$CT theorem :: POLYNOM3:20 for p be FinSequence of REAL for i be Element of NAT st i < len p holds Sum (p|(i+1)) = Sum (p|i) + p.(i+1); theorem :: POLYNOM3:21 for p be FinSequence of NAT for i,j,k1,k2 be Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p.(i+1) & k2 <= p.(j+1) & (Sum (p|i)) + k1 = (Sum (p|j)) + k2 holds i = j & k1 = k2; theorem :: POLYNOM3:22 for D1,D2 be set for f1 be FinSequence of D1* for f2 be FinSequence of D2* for i1,i2,j1,j2 be Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1.i1) & j2 in dom (f2.i2) & Card f1 = Card f2 & (Sum (( Card f1)|(i1-'1))) + j1 = (Sum ((Card f2)|(i2-'1))) + j2 holds i1 = i2 & j1 = j2; begin :: Polynomials definition let L be non empty ZeroStr; mode Polynomial of L is AlgSequence of L; end; theorem :: POLYNOM3:23 for L be non empty ZeroStr for p be Polynomial of L for n be Element of NAT holds n >= len p iff n is_at_least_length_of p; scheme :: POLYNOM3:sch 2 PolynomialLambdaF{R()->non empty addLoopStr, A()->Element of NAT, F(Element of NAT)->Element of R()}: ex p be Polynomial of R() st len p <= A() & for n be Element of NAT st n < A() holds p.n=F(n); registration let L be right_zeroed non empty addLoopStr; let p,q be Polynomial of L; cluster p+q -> finite-Support; end; theorem :: POLYNOM3:24 for L be right_zeroed non empty addLoopStr for p,q be Polynomial of L for n be Element of NAT holds (n is_at_least_length_of p & n is_at_least_length_of q) implies n is_at_least_length_of p+q; definition let L be Abelian non empty addLoopStr; let p,q be sequence of L; redefine func p+q; commutativity; end; ::$CT theorem :: POLYNOM3:26 for L be add-associative non empty addLoopStr for p,q,r be sequence of L holds p+q+r = p+(q+r); registration let L be add-associative right_zeroed right_complementable non empty addLoopStr; let p be Polynomial of L; cluster -p -> finite-Support; end; definition let L be non empty addLoopStr; let p,q be sequence of L; redefine func p-q equals :: POLYNOM3:def 6 p+-q; end; registration let L be add-associative right_zeroed right_complementable non empty addLoopStr; let p,q be Polynomial of L; cluster p-q -> finite-Support; end; theorem :: POLYNOM3:27 for L be non empty addLoopStr for p,q be sequence of L for n be Element of NAT holds (p-q).n = p.n - q.n; definition let L be non empty ZeroStr; func 0_.(L) -> sequence of L equals :: POLYNOM3:def 7 NAT --> 0.L; end; registration let L be non empty ZeroStr; cluster 0_.(L) -> finite-Support; end; theorem :: POLYNOM3:28 for L be right_zeroed non empty addLoopStr for p be sequence of L holds p+0_.(L) = p; theorem :: POLYNOM3:29 for L be add-associative right_zeroed right_complementable non empty addLoopStr for p be sequence of L holds p-p = 0_.(L); definition let L be non empty multLoopStr_0; func 1_.(L) -> sequence of L equals :: POLYNOM3:def 8 0_.(L)+*(0,1.L); end; registration let L be non empty multLoopStr_0; cluster 1_.(L) -> finite-Support; end; theorem :: POLYNOM3:30 for L be non empty multLoopStr_0 holds (1_.(L)).0 = 1.L & for n be Nat st n <> 0 holds (1_.(L)).n = 0.L; definition let L be non empty doubleLoopStr; let p,q be sequence of L; func p*'q -> sequence of L means :: POLYNOM3:def 9 for i be Element of NAT ex r be FinSequence of the carrier of L st len r = i+1 & it.i = Sum r & for k be Element of NAT st k in dom r holds r.k = p.(k-'1) * q.(i+1-'k); end; registration let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr; let p,q be Polynomial of L; cluster p*'q -> finite-Support; end; theorem :: POLYNOM3:31 for L be Abelian add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr for p,q,r be sequence of L holds p*'(q+r) = p*'q+p*'r; theorem :: POLYNOM3:32 for L be Abelian add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr for p,q,r be sequence of L holds (p+q)*'r = p*'r+q*'r; theorem :: POLYNOM3:33 for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive non empty doubleLoopStr for p,q,r be sequence of L holds p*'q*'r = p*'(q*'r); definition let L be Abelian add-associative right_zeroed commutative non empty doubleLoopStr; let p,q be sequence of L; redefine func p*'q; commutativity; end; theorem :: POLYNOM3:34 for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr for p be sequence of L holds p*'0_.(L) = 0_.(L); theorem :: POLYNOM3:35 for L be add-associative right_zeroed well-unital right_complementable right-distributive non empty doubleLoopStr for p be sequence of L holds p*'1_.(L) = p; begin :: The Ring of Polynomials definition let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr; func Polynom-Ring L -> strict non empty doubleLoopStr means :: POLYNOM3:def 10 (for x be set holds x in the carrier of it iff x is Polynomial of L) & (for x,y be Element of it, p,q be sequence of L st x = p & y = q holds x+y = p+q) & (for x,y be Element of it, p,q be sequence of L st x = p & y = q holds x*y = p*'q) & 0.it = 0_.(L) & 1.it = 1_.(L); end; registration let L be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr; cluster Polynom-Ring L -> Abelian; end; registration let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr; cluster Polynom-Ring L -> add-associative; cluster Polynom-Ring L -> right_zeroed; cluster Polynom-Ring L -> right_complementable; end; registration let L be Abelian add-associative right_zeroed right_complementable commutative distributive non empty doubleLoopStr; cluster Polynom-Ring L -> commutative; end; registration let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive non empty doubleLoopStr; cluster Polynom-Ring L -> associative; end; theorem :: POLYNOM3:36 for L be add-associative right_zeroed well-unital right_complementable left-distributive non empty doubleLoopStr for p be sequence of L holds (1_.(L))*'p = p; registration let L be add-associative right_zeroed right_complementable well-unital Abelian distributive non empty doubleLoopStr; cluster Polynom-Ring L -> well-unital; end; registration let L be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr; cluster Polynom-Ring L -> distributive; end; theorem :: POLYNOM3:37 for L being add-associative right_zeroed right_complementable well-unital Abelian distributive non empty doubleLoopStr holds 1.Polynom-Ring L = 1_.L;