:: Multivariate polynomials with arbitrary number of variables
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 22, 1999
:: Copyright (c) 1999-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, STRUCT_0, ZFMISC_1, RLVECT_1, ALGSTR_0, VECTSP_1,
XBOOLE_0, SUPINF_2, MESFUNC1, SUBSET_1, RELAT_1, FINSEQ_1, ARYTM_3,
PARTFUN1, TARSKI, CARD_3, NAT_1, ORDINAL4, FUNCT_1, FVSUM_1, ALGSTR_1,
BINOP_1, LATTICES, PRE_POLY, ALGSEQ_1, FINSET_1, ARYTM_1, FUNCOP_1,
GROUP_1, FUNCT_4, ORDINAL1, XXREAL_0, FINSEQ_2, MEMBER_1, FUNCT_2,
CARD_1, POLYNOM1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
FUNCT_1, PBOOLE, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, FINSEQ_1,
STRUCT_0, ALGSTR_0, FUNCT_3, XCMPLX_0, XXREAL_0, BINOP_1, NAT_1,
ALGSTR_1, RLVECT_1, FINSEQ_2, GROUP_1, VECTSP_1, FUNCOP_1, FUNCT_7,
MATRLIN, VFUNCT_1, FVSUM_1, PRE_POLY, RECDEF_1;
constructors BINOP_1, FINSEQOP, FINSEQ_4, RFUNCT_3, FUNCT_7, ALGSTR_1,
FVSUM_1, MATRLIN, RECDEF_1, RELSET_1, PBOOLE, VFUNCT_1, GROUP_1,
PRE_POLY;
registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, CARD_1,
MEMBERED, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, VALUED_0,
PRE_POLY, RELSET_1, VFUNCT_1, FUNCT_2, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
registration
cluster degenerated -> trivial
for add-associative right_zeroed right_complementable
right_unital right-distributive non empty doubleLoopStr;
end;
registration
cluster non trivial -> non degenerated
for add-associative right_zeroed right_complementable
right_unital right-distributive non empty doubleLoopStr;
end;
theorem :: POLYNOM1:1
for K being non empty addLoopStr, p1,p2 be FinSequence of the
carrier of K st dom p1 = dom p2 holds dom(p1+p2) = dom p1;
theorem :: POLYNOM1:2
for L being non empty addLoopStr, F being FinSequence of (the
carrier of L)* holds dom Sum F = dom F;
theorem :: POLYNOM1:3
for L being non empty addLoopStr, F being FinSequence of (the
carrier of L)* holds Sum (<*>((the carrier of L)*)) = <*>(the carrier of L);
theorem :: POLYNOM1:4
for L being non empty addLoopStr, p being Element of (the
carrier of L)* holds <*Sum p*> = Sum<*p*>;
theorem :: POLYNOM1:5
for L being non empty addLoopStr, F,G being FinSequence of (the
carrier of L)* holds Sum(F^G) = Sum F ^ Sum G;
definition
let L be non empty multMagma, p be FinSequence of the carrier of L,
a be Element of L;
redefine func a*p means
:: POLYNOM1:def 1
dom it = dom p & for i being object st i in dom p holds it/.i = a*(p/.i);
end;
definition
let L be non empty multMagma, 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 2
dom it = dom p & for i being object st i in dom p holds it/.i = (p/.i)*a;
end;
theorem :: POLYNOM1:6
for L being non empty multMagma, a being Element of L holds a*
<*>(the carrier of L) = <*>(the carrier of L);
theorem :: POLYNOM1:7
for L being non empty multMagma, a being Element of L holds (<*>
the carrier of L)*a = <*>(the carrier of L);
theorem :: POLYNOM1:8
for L being non empty multMagma, a, b being Element of L holds a
*<*b*> = <*a*b*>;
theorem :: POLYNOM1:9
for L being non empty multMagma, a, b being Element of L holds
<*b*>*a = <*b*a*>;
theorem :: POLYNOM1:10
for L being non empty multMagma, a being Element of L, p, q
being FinSequence of the carrier of L holds a*(p^q) = (a*p)^(a*q);
theorem :: POLYNOM1:11
for L being non empty multMagma, a being Element of L, p, q
being FinSequence of the carrier of L holds (p^q)*a = (p*a)^(q*a);
registration
cluster right_unital for non empty strict multLoopStr_0;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative distributive almost_left_invertible well-unital non
trivial for non empty doubleLoopStr;
end;
theorem :: POLYNOM1:12
for L being add-associative right_zeroed right_complementable
right_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:13
for L being add-associative right_zeroed right_complementable
right_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 --------------------------------------------------
theorem :: POLYNOM1:14
for L being add-associative right_zeroed right_complementable
non empty addLoopStr, F being FinSequence of (the carrier of L)* holds Sum
FlattenSeq F = Sum Sum F;
definition
let S be ZeroStr, f be (the carrier of S)-valued Function;
func Support f -> set means
:: POLYNOM1:def 3
for x being object holds x in it iff x in dom f & f.x <> 0.S;
end;
definition
let X be non empty set, S be non empty ZeroStr, f be Function of X, S;
redefine func Support f -> Subset of X means
:: POLYNOM1:def 4
for x being Element of X holds x in it iff f.x <> 0.S;
end;
definition
let S be ZeroStr, p be (the carrier of S)-valued Function;
attr p is finite-Support means
:: POLYNOM1:def 5
Support p is finite;
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;
begin :: Formal power series --------------------------------------------------
definition
let X be set, S be 1-sorted;
mode Series of X, S is Function of Bags X, S;
end;
definition
let n be set, L be non empty addLoopStr, p,q be Series of n, L;
func p+q -> Series of n, L equals
:: POLYNOM1:def 6
p + q;
end;
theorem :: POLYNOM1:15
for n being set, L being non empty addLoopStr, p,q being Series of n, L
for x being bag of n holds (p+q).x = p.x + q.x;
theorem :: POLYNOM1:16
for n being set, L being non empty addLoopStr, p,q,r being Series of n, L
st for x being bag of n holds r.x = p.x + q.x holds
r = p + q;
theorem :: POLYNOM1:17
for n being set,
L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being Series of n, L
for x being bag of n holds (-p).x = -(p.x);
theorem :: POLYNOM1:18
for n being set,
L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p,r being Series of n, L
st for x being bag of n holds r.x = -(p.x) holds
r = -p;
theorem :: POLYNOM1:19
for n be set, L be add-associative right_zeroed right_complementable
non empty addLoopStr, p be Series of n, L holds p = - -p;
theorem :: POLYNOM1:20
for n being set, L being right_zeroed non empty addLoopStr, 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 addLoopStr, p, q be
Series of n, L;
redefine func p+q;
commutativity;
end;
theorem :: POLYNOM1:21
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 addLoopStr, p, q be Series of n, L;
func p-q -> Series of n, L equals
:: POLYNOM1:def 7
p+-q;
end;
definition
let n be set, S be non empty ZeroStr;
func 0_(n, S) -> Series of n, S equals
:: POLYNOM1:def 8
(Bags n) --> 0.S;
end;
theorem :: POLYNOM1:22
for n being set, S being non empty ZeroStr, b be bag of n holds
(0_(n, S)).b = 0.S;
theorem :: POLYNOM1:23
for n being set, L be right_zeroed non empty addLoopStr, p be
Series of n, L holds p+0_(n,L) = p;
definition
let n be set, L be right_unital non empty multLoopStr_0;
func 1_(n,L) -> Series of n, L equals
:: POLYNOM1:def 9
0_(n,L)+*(EmptyBag n,1.L);
end;
theorem :: POLYNOM1:24
for n being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr, p being Series of n, L holds p-p =
0_(n,L);
theorem :: POLYNOM1:25
for n being set, L being right_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 10
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 Element of 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:26
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:27
for n being Ordinal, L being Abelian add-associative
right_zeroed right_complementable right_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:28
for n being Ordinal, L being add-associative right_complementable
right_zeroed right_unital distributive non empty doubleLoopStr, p being
Series of n, L holds p*'0_(n,L) = 0_(n,L);
theorem :: POLYNOM1:29
for n being Ordinal, L being add-associative
right_complementable right_zeroed distributive right_unital non trivial non
empty doubleLoopStr, p being Series of n, L holds p*'1_(n,L) = p;
theorem :: POLYNOM1:30
for n being Ordinal, L being add-associative
right_complementable right_zeroed distributive well-unital non trivial non
empty doubleLoopStr, p being Series of n, L holds 1_(n,L)*'p = p;
begin :: Polynomials ----------------------------------------------------------
registration
let n be set, S be non empty ZeroStr;
cluster finite-Support for 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;
registration
let n be Ordinal, L be right_zeroed non empty addLoopStr, p, q be
Polynomial of n, L;
cluster p+q -> finite-Support;
end;
registration
let n be Ordinal, L be add-associative right_zeroed right_complementable
non empty addLoopStr, p be Polynomial of n, L;
cluster -p -> finite-Support;
end;
registration
let n be Element of NAT, L be add-associative right_zeroed
right_complementable non empty addLoopStr, p, q be Polynomial of n, L;
cluster p-q -> finite-Support;
end;
registration
let n be Ordinal, S be non empty ZeroStr;
cluster 0_(n, S) -> finite-Support;
end;
registration
let n be Ordinal, L be add-associative right_zeroed right_complementable
right_unital right-distributive non trivial doubleLoopStr;
cluster 1_(n,L) -> finite-Support;
end;
registration
let n be Ordinal, L be add-associative right_complementable right_zeroed
right_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
right_unital distributive non trivial doubleLoopStr;
func Polynom-Ring (n, L) -> strict non empty doubleLoopStr means
:: POLYNOM1:def 11
(
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;
registration
let n be Ordinal, L be Abelian right_zeroed add-associative
right_complementable right_unital distributive non trivial
doubleLoopStr;
cluster Polynom-Ring (n, L) -> Abelian;
end;
registration
let n be Ordinal, L be add-associative right_zeroed right_complementable
right_unital distributive non trivial doubleLoopStr;
cluster Polynom-Ring (n, L) -> add-associative;
end;
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
right_unital distributive non trivial doubleLoopStr;
cluster Polynom-Ring (n, L) -> right_zeroed;
end;
registration
let n be Ordinal, L be right_complementable right_zeroed add-associative
right_unital distributive non trivial doubleLoopStr;
cluster Polynom-Ring (n, L) -> right_complementable;
end;
registration
let n be Ordinal, L be Abelian add-associative right_zeroed
right_complementable commutative right_unital distributive non trivial non
empty doubleLoopStr;
cluster Polynom-Ring (n, L) -> commutative;
end;
registration
let n be Ordinal, L be Abelian add-associative right_zeroed
right_complementable right_unital distributive associative non trivial non
empty doubleLoopStr;
cluster Polynom-Ring (n, L) -> associative;
end;
registration
let n be Ordinal, L be right_zeroed Abelian add-associative
right_complementable well-unital distributive associative non trivial non
empty doubleLoopStr;
cluster Polynom-Ring (n, L) -> well-unital right-distributive;
end;
theorem :: POLYNOM1:31
for n being Ordinal, L being right_zeroed Abelian add-associative
right_complementable right_unital distributive associative non trivial non
empty doubleLoopStr holds 1.Polynom-Ring(n, L) = 1_(n,L);