Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### Multivariate Polynomials with Arbitrary Number of Variables

**by****Piotr Rudnicki, and****Andrzej Trybulec**- Received September 22, 1999
- MML identifier: POLYNOM1

- [ Mizar article, MML identifier index ]

environ vocabulary MONOID_0, FUNCT_1, VECTSP_1, RELAT_1, BINOP_1, FUNCOP_1, PARTFUN1, ARYTM_1, RLVECT_1, FINSEQ_1, BOOLE, FUNCT_4, CAT_1, PBOOLE, CARD_1, FINSEQ_2, ORDERS_2, WELLORD1, ORDERS_1, RELAT_2, FINSET_1, TRIANG_1, MATRLIN, MEASURE6, SQUARE_1, CARD_3, REALSET1, GROUP_1, ALGSTR_1, LATTICES, DTCONSTR, MSUALG_3, SEQM_3, ALGSEQ_1, ORDINAL1, ARYTM_3, FUNCT_2, FRAENKEL, FINSUB_1, SETWISEO, TARSKI, RFINSEQ, POLYNOM1, FVSUM_1, FINSEQ_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, STRUCT_0, RELAT_1, RELSET_1, RELAT_2, FUNCT_1, FINSET_1, FINSUB_1, SETWISEO, ORDINAL1, PBOOLE, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_4, NAT_1, REALSET1, ALGSTR_1, RLVECT_1, ORDERS_1, ORDERS_2, FINSEQ_1, FINSEQ_2, WELLORD1, SEQM_3, CARD_1, CARD_3, FINSEQ_4, CQC_LANG, VECTSP_1, GROUP_1, TRIANG_1, TREES_4, WSIERP_1, MONOID_0, MSUALG_3, FUNCOP_1, FUNCT_7, FRAENKEL, DTCONSTR, BINARITH, MATRLIN, RFUNCT_3, RFINSEQ, TOPREAL1, FVSUM_1; constructors ORDERS_2, WELLORD2, CQC_LANG, WELLFND1, TRIANG_1, FINSEQOP, REAL_1, FUNCT_7, DOMAIN_1, BINARITH, MATRLIN, MSUALG_3, WSIERP_1, TOPREAL1, ALGSTR_2, FVSUM_1, SETWOP_2, SETWISEO, MONOID_0, MEMBERED; clusters XREAL_0, STRUCT_0, RELAT_1, FUNCT_1, FINSET_1, RELSET_1, CARD_3, FINSEQ_5, CARD_1, ALGSTR_1, ALGSTR_2, FUNCOP_1, FINSEQ_1, FINSEQ_2, PRALG_1, CIRCCOMB, CQC_LANG, BINARITH, ORDINAL3, HEYTING2, MONOID_0, GOBRD13, VECTSP_1, FRAENKEL, MEMBERED, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Basics --------------------------------------------------------------- theorem :: POLYNOM1:1 for i, j being Nat holds multnat.(i,j) = i*j; theorem :: POLYNOM1:2 for X being set, A being non empty set, F being BinOp of A, f being Function of X, A, x being Element of A holds dom (F[:](f,x)) = X; theorem :: POLYNOM1:3 for a, b, c being Nat holds a-'b-'c = a-'(b+c); theorem :: POLYNOM1:4 for X being set, R being Relation st field R c= X holds R is Relation of X; theorem :: POLYNOM1:5 for K being non empty LoopStr, p1,p2 be FinSequence of the carrier of K st dom p1 = dom p2 holds dom(p1+p2) = dom p1; theorem :: POLYNOM1:6 for f being Function, x,y being set holds rng (f+*(x,y)) c= rng f \/ {y}; definition let A, B be set, f be Function of A, B, x be set, y be Element of B; redefine func f+*(x,y) -> Function of A, B; end; definition let X be set, f be ManySortedSet of X, x, y be set; redefine func f+*(x,y) -> ManySortedSet of X; end; theorem :: POLYNOM1:7 for f being one-to-one Function holds Card (f qua set) = Card rng f; definition let A be non empty set; let F, G be BinOp of A, z, u be Element of A; cluster doubleLoopStr(# A, F, G, z, u #) -> non empty; end; definition let A be set; let X be set, D be FinSequence-DOMAIN of A, p be PartFunc of X,D, i be set; redefine func p/.i -> Element of D; end; definition let X be set, S be 1-sorted; mode Function of X, S is Function of X, the carrier of S; canceled; end; definition let X be set; cluster being_linear-order well-ordering Order of X; end; theorem :: POLYNOM1:8 for X being non empty set, A being non empty finite Subset of X, R being Order of X, x being Element of X st x in A & R linearly_orders A & for y being Element of X st y in A holds [x,y] in R holds (SgmX (R,A))/.1 = x; theorem :: POLYNOM1:9 for X being non empty set, A being non empty finite Subset of X, R being Order of X, x being Element of X st x in A & R linearly_orders A & for y being Element of X st y in A holds [y,x] in R holds SgmX (R,A)/.len SgmX (R,A) = x; definition let X be non empty set, A be non empty finite Subset of X, R be being_linear-order Order of X; cluster SgmX(R, A) -> non empty one-to-one; end; definition cluster {} -> FinSequence-yielding; end; definition cluster FinSequence-yielding FinSequence; end; definition let F, G be FinSequence-yielding FinSequence; redefine func F^^G -> FinSequence-yielding FinSequence; end; definition let i be Nat, f be FinSequence; cluster i |-> f -> FinSequence-yielding; end; definition let F be FinSequence-yielding FinSequence, x be set; cluster F.x -> FinSequence-like; end; definition let F be FinSequence; cluster Card F -> FinSequence-like; end; definition cluster Cardinal-yielding FinSequence; end; theorem :: POLYNOM1:10 for f being Function holds f is Cardinal-yielding iff for y being set st y in rng f holds y is Cardinal; definition let F, G be Cardinal-yielding FinSequence; cluster F^G -> Cardinal-yielding; end; definition cluster -> Cardinal-yielding FinSequence of NAT; end; definition cluster Cardinal-yielding FinSequence of NAT; end; definition let D be set; let F be FinSequence of D*; redefine func Card F -> Cardinal-yielding FinSequence of NAT; end; definition let F be FinSequence of NAT, i be Nat; cluster F|i -> Cardinal-yielding; end; theorem :: POLYNOM1:11 for F being Function, X being set holds Card (F|X) = (Card F)|X; definition let F be empty Function; cluster Card F -> empty; end; theorem :: POLYNOM1:12 for p being set holds Card <*p*> = <*Card p*>; theorem :: POLYNOM1:13 for F, G be FinSequence holds Card (F^G) = Card F ^ Card G; definition let X be set; cluster <*>X -> FinSequence-yielding; end; definition let f be FinSequence; cluster <*f*> -> FinSequence-yielding; end; theorem :: POLYNOM1:14 for f being Function holds f is FinSequence-yielding iff for y being set st y in rng f holds y is FinSequence; definition let F, G be FinSequence-yielding FinSequence; cluster F^G -> FinSequence-yielding; end; theorem :: POLYNOM1:15 for L being non empty LoopStr, F being FinSequence of (the carrier of L)* holds dom Sum F = dom F; theorem :: POLYNOM1:16 for L being non empty LoopStr, F being FinSequence of (the carrier of L)* holds Sum (<*>((the carrier of L)*)) = <*>(the carrier of L); theorem :: POLYNOM1:17 for L being non empty LoopStr, p being Element of (the carrier of L)* holds <*Sum p*> = Sum<*p*>; theorem :: POLYNOM1:18 for L being non empty LoopStr, F,G being FinSequence of (the carrier of L)* holds Sum(F^G) = Sum F ^ Sum G; definition let L be non empty HGrStr, p be FinSequence of the carrier of L, a be Element of L; redefine func a*p -> FinSequence of the carrier of L means :: POLYNOM1:def 2 dom it = dom p & for i being set st i in dom p holds it/.i = a*(p/.i); end; definition let L be non empty HGrStr, p be FinSequence of the carrier of L, a be Element of L; func p*a -> FinSequence of the carrier of L means :: POLYNOM1:def 3 dom it = dom p & for i being set st i in dom p holds it/.i = (p/.i)*a; end; theorem :: POLYNOM1:19 for L being non empty HGrStr, a being Element of L holds a*<*>(the carrier of L) = <*>(the carrier of L); theorem :: POLYNOM1:20 for L being non empty HGrStr, a being Element of L holds (<*>the carrier of L)*a = <*>(the carrier of L); theorem :: POLYNOM1:21 for L being non empty HGrStr, a, b being Element of L holds a*<*b*> = <*a*b*>; theorem :: POLYNOM1:22 for L being non empty HGrStr, a, b being Element of L holds <*b*>*a = <*b*a*>; theorem :: POLYNOM1:23 for L being non empty HGrStr, a being Element of L, p, q being FinSequence of the carrier of L holds a*(p^q) = (a*p)^(a*q); theorem :: POLYNOM1:24 for L being non empty HGrStr, a being Element of L, p, q being FinSequence of the carrier of L holds (p^q)*a = (p*a)^(q*a); definition cluster non degenerated -> non trivial (non empty multLoopStr_0); end; definition cluster unital (non empty strict multLoopStr_0); end; definition cluster strict Abelian add-associative right_zeroed right_complementable associative commutative distributive Field-like unital non trivial (non empty doubleLoopStr); end; canceled 2; theorem :: POLYNOM1:27 for L being add-associative right_zeroed right_complementable unital right-distributive (non empty doubleLoopStr) st 0.L = 1.L holds L is trivial; theorem :: POLYNOM1:28 for L being add-associative right_zeroed right_complementable unital distributive (non empty doubleLoopStr), a being Element of L, p being FinSequence of the carrier of L holds Sum (a*p) = a*Sum p; theorem :: POLYNOM1:29 for L being add-associative right_zeroed right_complementable unital distributive (non empty doubleLoopStr), a being Element of L, p being FinSequence of the carrier of L holds Sum (p*a) = (Sum p)*a; begin :: Sequence flattening -------------------------------------------------- definition let D be set, F be empty FinSequence of D*; cluster FlattenSeq F -> empty; end; theorem :: POLYNOM1:30 for D being set, F being FinSequence of D* holds len FlattenSeq F = Sum Card F; theorem :: POLYNOM1:31 for D, E being set, F being FinSequence of D*, G being FinSequence of E* st Card F = Card G holds len FlattenSeq F = len FlattenSeq G; theorem :: POLYNOM1:32 for D being set, F being FinSequence of D*, k being set st k in dom FlattenSeq F ex i, j being Nat st i in dom F & j in dom (F.i) & k = (Sum Card (F|(i-'1))) + j & (F.i).j = (FlattenSeq F).k; theorem :: POLYNOM1:33 for D being set, F being FinSequence of D*, i, j being Nat st i in dom F & j in dom (F.i) holds (Sum Card (F|(i-'1))) + j in dom FlattenSeq F & (F.i).j = (FlattenSeq F).((Sum Card (F|(i-'1))) + j); theorem :: POLYNOM1:34 for L being add-associative right_zeroed right_complementable (non empty LoopStr), F being FinSequence of (the carrier of L)* holds Sum FlattenSeq F = Sum Sum F; theorem :: POLYNOM1:35 for X, Y being non empty set, f being FinSequence of X*, v being Function of X, Y holds (dom f --> v)**f is FinSequence of Y*; theorem :: POLYNOM1:36 for X, Y being non empty set, f being FinSequence of X*, v being Function of X, Y ex F being FinSequence of Y* st F = (dom f --> v)**f & v*FlattenSeq f = FlattenSeq F; begin :: Functions yielding natural numbers ----------------------------------- definition cluster {} -> natural-yielding; end; definition cluster natural-yielding Function; end; definition let f be natural-yielding Function; let x be set; redefine func f.x -> Nat; end; definition let f be natural-yielding Function, x be set, n be Nat; cluster f+*(x,n) -> natural-yielding; end; definition let X be set; cluster -> natural-yielding Function of X, NAT; end; definition let X be set; cluster natural-yielding ManySortedSet of X; end; definition let X be set, b1, b2 be natural-yielding ManySortedSet of X; canceled; func b1+b2 -> ManySortedSet of X means :: POLYNOM1:def 5 for x being set holds it.x = b1.x+b2.x; commutativity; func b1 -' b2 -> ManySortedSet of X means :: POLYNOM1:def 6 for x being set holds it.x = b1.x -' b2.x; end; theorem :: POLYNOM1:37 for X being set, b, b1, b2 being natural-yielding ManySortedSet of X st for x being set st x in X holds b.x = b1.x+b2.x holds b = b1+b2; theorem :: POLYNOM1:38 for X being set, b, b1, b2 being natural-yielding ManySortedSet of X st for x being set st x in X holds b.x = b1.x-'b2.x holds b = b1-'b2; definition let X be set, b1, b2 be natural-yielding ManySortedSet of X; cluster b1+b2 -> natural-yielding; cluster b1-'b2 -> natural-yielding; end; theorem :: POLYNOM1:39 for X being set, b1, b2, b3 being natural-yielding ManySortedSet of X holds (b1+b2)+b3 = b1+(b2+b3); theorem :: POLYNOM1:40 for X being set, b, c, d being natural-yielding ManySortedSet of X holds b-'c-'d = b-'(c+d); begin :: The support of a function -------------------------------------------- definition let f be Function; func support f means :: POLYNOM1:def 7 for x being set holds x in it iff f.x <> 0; end; theorem :: POLYNOM1:41 for f being Function holds support f c= dom f; definition let f be Function; attr f is finite-support means :: POLYNOM1:def 8 support f is finite; synonym f has_finite-support; end; definition cluster {} -> finite-support; end; definition cluster finite -> finite-support Function; end; definition cluster natural-yielding finite-support non empty Function; end; definition let f be finite-support Function; cluster support f -> finite; end; definition let X be set; cluster finite-support Function of X, NAT; end; definition let f be finite-support Function, x, y be set; cluster f+*(x,y) -> finite-support; end; definition let X be set; cluster natural-yielding finite-support ManySortedSet of X; end; theorem :: POLYNOM1:42 for X being set, b1, b2 being natural-yielding ManySortedSet of X holds support (b1+b2) = support b1 \/ support b2; theorem :: POLYNOM1:43 for X being set, b1, b2 being natural-yielding ManySortedSet of X holds support (b1-'b2) c= support b1; definition let X be non empty set, S be ZeroStr, f be Function of X, S; func Support f -> Subset of X means :: POLYNOM1:def 9 for x being Element of X holds x in it iff f.x <> 0.S; end; definition let X be non empty set, S be ZeroStr, p be Function of X, S; attr p is finite-Support means :: POLYNOM1:def 10 Support p is finite; synonym p has_finite-Support; end; begin :: Bags ----------------------------------------------------------------- definition let X be set; mode bag of X is natural-yielding finite-support ManySortedSet of X; end; definition let X be finite set; cluster -> finite-support ManySortedSet of X; end; definition let X be set, b1, b2 be bag of X; cluster b1+b2 -> finite-support; cluster b1-'b2 -> finite-support; end; theorem :: POLYNOM1:44 for X being set holds X--> 0 is bag of X; definition let n be Ordinal, p, q be bag of n; pred p < q means :: POLYNOM1:def 11 ex k being Ordinal st p.k < q.k & for l being Ordinal st l in k holds p.l = q.l; asymmetry; end; theorem :: POLYNOM1:45 for n being Ordinal, p, q, r being bag of n st p < q & q < r holds p < r; definition let n be Ordinal, p, q be bag of n; pred p <=' q means :: POLYNOM1:def 12 p < q or p = q; reflexivity; end; theorem :: POLYNOM1:46 for n being Ordinal, p, q, r being bag of n st p <=' q & q <=' r holds p <=' r ; theorem :: POLYNOM1:47 for n being Ordinal, p, q, r being bag of n st p < q & q <=' r holds p < r; theorem :: POLYNOM1:48 for n being Ordinal, p, q, r being bag of n st p <=' q & q < r holds p < r; theorem :: POLYNOM1:49 for n being Ordinal, p, q being bag of n holds p <=' q or q <=' p; definition let X be set, d, b be bag of X; pred d divides b means :: POLYNOM1:def 13 for k being set holds d.k <= b.k; reflexivity; end; theorem :: POLYNOM1:50 for n being set, d, b being bag of n st for k being set st k in n holds d.k <= b.k holds d divides b; theorem :: POLYNOM1:51 for n being Ordinal, b1, b2 being bag of n st b1 divides b2 holds b2 -' b1 + b1 = b2; theorem :: POLYNOM1:52 for X being set, b1, b2 being bag of X holds b2 + b1 -' b1 = b2; theorem :: POLYNOM1:53 for n being Ordinal, d, b being bag of n st d divides b holds d <=' b; theorem :: POLYNOM1:54 for n being set, b,b1,b2 being bag of n st b = b1 + b2 holds b1 divides b; definition let X be set; func Bags X means :: POLYNOM1:def 14 for x being set holds x in it iff x is bag of X; end; definition let X be set; redefine func Bags X -> Subset of Bags X; end; theorem :: POLYNOM1:55 Bags {} = {{}}; definition let X be set; cluster Bags X -> non empty; end; definition let X be set, B be non empty Subset of Bags X; redefine mode Element of B -> bag of X; end; definition let n be set, L be non empty 1-sorted, p be Function of Bags n, L, x be bag of n; redefine func p.x -> Element of L; end; definition let X be set; func EmptyBag X -> Element of Bags X equals :: POLYNOM1:def 15 X --> 0; end; theorem :: POLYNOM1:56 for X, x being set holds (EmptyBag X).x = 0; theorem :: POLYNOM1:57 for X be set, b being bag of X holds b+EmptyBag X = b; theorem :: POLYNOM1:58 for X be set, b being bag of X holds b-'EmptyBag X = b; theorem :: POLYNOM1:59 for X be set, b being bag of X holds (EmptyBag X) -' b = EmptyBag X; theorem :: POLYNOM1:60 for X being set, b being bag of X holds b-'b = EmptyBag X; theorem :: POLYNOM1:61 for n being set, b1, b2 be bag of n st b1 divides b2 & b2 -' b1 = EmptyBag n holds b2 = b1; theorem :: POLYNOM1:62 for n being set, b being bag of n st b divides EmptyBag n holds EmptyBag n = b; theorem :: POLYNOM1:63 for n being set, b being bag of n holds EmptyBag n divides b; theorem :: POLYNOM1:64 for n being Ordinal, b being bag of n holds EmptyBag n <=' b; definition let n be Ordinal; func BagOrder n -> Order of Bags n means :: POLYNOM1:def 16 for p, q being bag of n holds [p, q] in it iff p <=' q; end; definition let n be Ordinal; cluster BagOrder n -> being_linear-order; end; definition let X be set, f be Function of X, NAT; func NatMinor f -> Subset of Funcs(X, NAT) means :: POLYNOM1:def 17 for g being natural-yielding ManySortedSet of X holds g in it iff for x being set st x in X holds g.x <= f.x; end; theorem :: POLYNOM1:65 for X being set, f being Function of X, NAT holds f in NatMinor f; definition let X be set, f be Function of X, NAT; cluster NatMinor f -> non empty functional; end; definition let X be set, f be Function of X, NAT; cluster -> natural-yielding Element of NatMinor f; end; theorem :: POLYNOM1:66 for X being set, f being finite-support Function of X, NAT holds NatMinor f c= Bags X; definition let X be set, f be finite-support Function of X, NAT; redefine func support f -> Element of Fin X; end; theorem :: POLYNOM1:67 for X being non empty set, f being finite-support Function of X, NAT holds Card NatMinor f = multnat $$ (support f, addnat[:](f,1)); definition let X be set, f be finite-support Function of X, NAT; cluster NatMinor f -> finite; end; definition let n be Ordinal, b be bag of n; func divisors b -> FinSequence of Bags n means :: POLYNOM1:def 18 ex S being non empty finite Subset of Bags n st it = SgmX(BagOrder n, S) & for p being bag of n holds p in S iff p divides b; end; definition let n be Ordinal, b be bag of n; cluster divisors b -> non empty one-to-one; end; theorem :: POLYNOM1:68 for n being Ordinal,i being Nat, b being bag of n st i in dom divisors b holds ((divisors b)/.i) qua Element of Bags n divides b; theorem :: POLYNOM1:69 for n being Ordinal, b being bag of n holds (divisors b)/.1 = EmptyBag n & (divisors b)/.len divisors b = b; theorem :: POLYNOM1:70 for n being Ordinal, i being Nat, b, b1, b2 being bag of n st i > 1 & i < len divisors b holds (divisors b)/.i <> EmptyBag n & (divisors b)/.i <> b; theorem :: POLYNOM1:71 for n being Ordinal holds divisors EmptyBag n = <* EmptyBag n *>; definition let n be Ordinal, b be bag of n; func decomp b -> FinSequence of 2-tuples_on Bags n means :: POLYNOM1:def 19 dom it = dom divisors b & for i being Nat, p being bag of n st i in dom it & p = (divisors b)/.i holds it/.i = <*p, b-'p*>; end; theorem :: POLYNOM1:72 for n being Ordinal, i being Nat, b being bag of n st i in dom decomp b ex b1, b2 being bag of n st (decomp b)/.i = <*b1, b2*> & b = b1+b2; theorem :: POLYNOM1:73 for n being Ordinal, b, b1, b2 being bag of n st b = b1+b2 ex i being Nat st i in dom decomp b & (decomp b)/.i = <*b1, b2*>; theorem :: POLYNOM1:74 for n being Ordinal, i being Nat, b,b1,b2 being bag of n st i in dom decomp b & (decomp b)/.i = <*b1, b2*> holds b1 = (divisors b)/.i; definition let n be Ordinal, b be bag of n; cluster decomp b -> non empty one-to-one FinSequence-yielding; end; definition let n be Ordinal, b be Element of Bags n; cluster decomp b -> non empty one-to-one FinSequence-yielding; end; theorem :: POLYNOM1:75 for n being Ordinal, b being bag of n holds (decomp b)/.1 = <*EmptyBag n, b*> & (decomp b)/.len decomp b = <*b, EmptyBag n*>; theorem :: POLYNOM1:76 for n being Ordinal, i being Nat, b, b1, b2 being bag of n st i > 1 & i < len decomp b & (decomp b)/.i = <*b1, b2*> holds b1 <> EmptyBag n & b2 <> EmptyBag n; theorem :: POLYNOM1:77 for n being Ordinal holds decomp EmptyBag n = <* <*EmptyBag n, EmptyBag n*> *> ; theorem :: POLYNOM1:78 for n being Ordinal, b being bag of n, f, g being FinSequence of (3-tuples_on Bags n)* st dom f = dom decomp b & dom g = dom decomp b & (for k being Nat st k in dom f holds f.k = ((decomp ((((decomp b)/.k)/.1) qua Element of Bags n))) ^^ ((len (decomp ((((decomp b)/.k)/.1) qua Element of Bags n))) |-> <*(((decomp b)/.k)/.2)*>)) & (for k being Nat st k in dom g holds g.k = ((len (decomp ((((decomp b)/.k)/.2) qua Element of Bags n))) |-> <*((decomp b)/.k)/.1*>) ^^ (decomp ((((decomp b)/.k)/.2) qua Element of Bags n))) ex p being Permutation of dom FlattenSeq f st FlattenSeq g = (FlattenSeq f)*p; begin :: Formal power series -------------------------------------------------- definition let X be set, S be 1-sorted; mode Series of X, S is Function of Bags X, S; canceled; end; definition let n be set, L be non empty LoopStr, p, q be Series of n, L; func p+q -> Series of n, L means :: POLYNOM1:def 21 for x being bag of n holds it.x = p.x+q.x; end; theorem :: POLYNOM1:79 for n being set, L being right_zeroed (non empty LoopStr), p, q being Series of n, L holds Support (p+q) c= Support p \/ Support q; definition let n be set, L be Abelian right_zeroed (non empty LoopStr), p, q be Series of n, L; redefine func p+q; commutativity; end; theorem :: POLYNOM1:80 for n being set, L being add-associative right_zeroed (non empty doubleLoopStr), p, q, r being Series of n, L holds (p+q)+r = p+(q+r); definition let n be set, L be add-associative right_zeroed right_complementable (non empty LoopStr), p be Series of n, L; func -p -> Series of n, L means :: POLYNOM1:def 22 for x being bag of n holds it.x = -(p.x); involutiveness; end; definition let n be set, L be add-associative right_zeroed right_complementable (non empty LoopStr), p, q be Series of n, L; func p-q -> Series of n, L equals :: POLYNOM1:def 23 p+-q; end; definition let n be set, S be non empty ZeroStr; func 0_(n, S) -> Series of n, S equals :: POLYNOM1:def 24 (Bags n) --> 0.S; end; theorem :: POLYNOM1:81 for n being set, S being non empty ZeroStr, b be bag of n holds (0_(n, S)).b = 0.S; theorem :: POLYNOM1:82 for n being set, L be right_zeroed (non empty LoopStr), p be Series of n, L holds p+0_(n,L) = p; definition let n be set, L be unital (non empty multLoopStr_0); func 1_(n,L) -> Series of n, L equals :: POLYNOM1:def 25 0_(n,L)+*(EmptyBag n,1.L); end; theorem :: POLYNOM1:83 for n being set, L being add-associative right_zeroed right_complementable (non empty LoopStr), p being Series of n, L holds p-p = 0_(n,L); theorem :: POLYNOM1:84 for n being set, L being unital (non empty multLoopStr_0) holds (1_(n,L)).EmptyBag n = 1.L & for b being bag of n st b <> EmptyBag n holds (1_(n,L)).b = 0.L; definition let n be Ordinal, L be add-associative right_complementable right_zeroed (non empty doubleLoopStr), p, q be Series of n, L; func p*'q -> Series of n, L means :: POLYNOM1:def 26 for b being bag of n ex s being FinSequence of the carrier of L st it.b = Sum s & len s = len decomp b & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2; end; theorem :: POLYNOM1:85 for n being Ordinal, L being Abelian add-associative right_zeroed right_complementable distributive associative (non empty doubleLoopStr), p, q, r being Series of n, L holds p*'(q+r) = p*'q+p*'r; theorem :: POLYNOM1:86 for n being Ordinal, L being Abelian add-associative right_zeroed right_complementable unital distributive associative (non empty doubleLoopStr), p, q, r being Series of n, L holds (p*'q)*'r = p*'(q*'r); definition let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable commutative (non empty doubleLoopStr), p, q be Series of n, L; redefine func p*'q; commutativity; end; theorem :: POLYNOM1:87 for n being Ordinal, L being add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), p being Series of n, L holds p*'0_(n,L) = 0_(n,L); theorem :: POLYNOM1:88 for n being Ordinal, L being add-associative right_complementable right_zeroed distributive unital non trivial (non empty doubleLoopStr), p being Series of n, L holds p*'1_(n,L) = p; theorem :: POLYNOM1:89 for n being Ordinal, L being add-associative right_complementable right_zeroed distributive unital non trivial (non empty doubleLoopStr), p being Series of n, L holds 1_(n,L)*'p = p; begin :: Polynomials ---------------------------------------------------------- definition let n be set, S be non empty ZeroStr; cluster finite-Support Series of n, S; end; definition let n be Ordinal, S be non empty ZeroStr; mode Polynomial of n, S is finite-Support Series of n, S; end; definition let n be Ordinal, L be right_zeroed (non empty LoopStr), p, q be Polynomial of n, L; cluster p+q -> finite-Support; end; definition let n be Ordinal, L be add-associative right_zeroed right_complementable (non empty LoopStr), p be Polynomial of n, L; cluster -p -> finite-Support; end; definition let n be Nat, L be add-associative right_zeroed right_complementable (non empty LoopStr), p, q be Polynomial of n, L; cluster p-q -> finite-Support; end; definition let n be Ordinal, S be non empty ZeroStr; cluster 0_(n, S) -> finite-Support; end; definition let n be Ordinal, L be add-associative right_zeroed right_complementable unital right-distributive non trivial (non empty doubleLoopStr); cluster 1_(n,L) -> finite-Support; end; definition let n be Ordinal, L be add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), p, q be Polynomial of n, L; cluster p*'q -> finite-Support; end; begin :: The ring of polynomials --------------------------------------------- definition let n be Ordinal, L be right_zeroed add-associative right_complementable unital distributive non trivial (non empty doubleLoopStr); func Polynom-Ring (n, L) -> strict non empty doubleLoopStr means :: POLYNOM1:def 27 (for x being set holds x in the carrier of it iff x is Polynomial of n, L) & (for x, y being Element of it, p, q being Polynomial of n, L st x = p & y = q holds x+y = p+q) & (for x, y being Element of it, p, q being Polynomial of n, L st x = p & y = q holds x*y = p*'q) & 0.it = 0_(n,L) & 1_ it = 1_(n,L); end; definition let n be Ordinal, L be Abelian right_zeroed add-associative right_complementable unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> Abelian; end; definition let n be Ordinal, L be add-associative right_zeroed right_complementable unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> add-associative; end; definition let n be Ordinal, L be right_zeroed add-associative right_complementable unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> right_zeroed; end; definition let n be Ordinal, L be right_complementable right_zeroed add-associative unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> right_complementable; end; definition let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable commutative unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> commutative; end; definition let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable unital distributive associative non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> associative; end; definition let n be Ordinal, L be right_zeroed Abelian add-associative right_complementable unital distributive associative non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> unital right-distributive; end;

Back to top