Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
The abstract of the Mizar article:
-
- 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