:: More About Polynomials: Monomials and Constant Polynomials
:: by Christoph Schwarzweller
::
:: Received November 28, 2001
:: Copyright (c) 2001-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 RLVECT_1, ALGSTR_1, ALGSTR_0, VECTSP_1, BINOP_1, LATTICES,
VECTSP_2, ZFMISC_1, XBOOLE_0, STRUCT_0, POLYNOM1, VALUED_0, SUBSET_1,
SUPINF_2, FUNCT_4, PRE_POLY, FUNCT_1, FUNCOP_1, RELAT_1, ORDINAL1,
CARD_1, PARTFUN1, POLYNOM2, FINSEQ_1, CARD_3, NUMBERS, XXREAL_0,
FINSET_1, ORDERS_1, ARYTM_3, NAT_1, MESFUNC1, QUOFIELD, GROUP_1, TARSKI,
MSSUBFAM, ALGSEQ_1, CAT_3, XCMPLX_0, ORDINAL4, POLYNOM7, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
FINSET_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_7, POLYNOM1, NUMBERS,
XXREAL_0, DOMAIN_1, STRUCT_0, ALGSTR_0, FUNCT_4, NAT_1, ALGSTR_1,
RLVECT_1, ORDERS_1, FINSEQ_1, FUNCOP_1, GROUP_1, QUOFIELD, GRCAT_1,
VECTSP_2, POLYNOM2, VECTSP_1, GROUP_6, PRE_POLY;
constructors REALSET2, GRCAT_1, GROUP_6, TRIANG_1, QUOFIELD, POLYNOM2,
ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, FUNCT_4, RINGCAT1, MOD_4;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0,
STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM1, POLYNOM2, ALGSTR_0, CARD_1,
SUBSET_1, PRE_POLY, FUNCT_1, RINGCAT1, MOD_4;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin
registration
cluster Abelian left_zeroed right_zeroed add-associative
right_complementable well-unital associative commutative distributive
domRing-like for non trivial doubleLoopStr;
end;
definition
let X be set, R be non empty ZeroStr, p be Series of X,R;
attr p is non-zero means
:: POLYNOM7:def 1
p <> 0_(X,R);
end;
registration
let X be set, R be non trivial ZeroStr;
cluster non-zero for Series of X,R;
end;
registration
let n be Ordinal, R be non trivial ZeroStr;
cluster non-zero for Polynomial of n,R;
end;
theorem :: POLYNOM7:1
for X being set, R being non empty ZeroStr, s being Series of X,R
holds s = 0_(X,R) iff Support s = {};
theorem :: POLYNOM7:2
for X being set, R being non empty ZeroStr holds R is non trivial iff
ex s being Series of X,R st Support(s) <> {};
definition
let X be set, b be bag of X;
attr b is univariate means
:: POLYNOM7:def 2
ex u being Element of X st support b = {u};
end;
registration
let X be non empty set;
cluster univariate for bag of X;
end;
registration
let X be non empty set;
cluster univariate -> non empty-yielding for bag of X;
end;
begin :: Polynomials without Variables
theorem :: POLYNOM7:3
for b being bag of {} holds b = EmptyBag {};
theorem :: POLYNOM7:4
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p being Polynomial of {},
L, x being Function of {},L holds eval(p,x) = p.(EmptyBag{});
theorem :: POLYNOM7:5
for L being right_zeroed add-associative right_complementable Abelian
well-unital distributive associative non trivial non trivial doubleLoopStr
holds Polynom-Ring({},L) is_ringisomorph_to L;
begin :: Monomials
definition
let X be set, L be non empty ZeroStr, p be Series of X,L;
attr p is monomial-like means
:: POLYNOM7:def 3
ex b being bag of X st for b9 being bag of X st b9 <> b holds p.b9 = 0.L;
end;
registration
let X be set, L be non empty ZeroStr;
cluster monomial-like for Series of X,L;
end;
definition
let X be set, L be non empty ZeroStr;
mode Monomial of X,L is monomial-like Series of X,L;
end;
registration
let X be set, L be non empty ZeroStr;
cluster monomial-like -> finite-Support for Series of X,L;
end;
theorem :: POLYNOM7:6
for X being set, L being non empty ZeroStr, p being Series of X,L
holds p is Monomial of X,L iff (Support p = {} or ex b being bag of X st
Support p = {b});
definition
let X be set, L be non empty ZeroStr, a be Element of L, b be bag of X;
func Monom(a,b) -> Monomial of X,L equals
:: POLYNOM7:def 4
0_(X,L)+*(b,a);
end;
definition
let X be set, L be non empty ZeroStr, m be Monomial of X,L;
func term(m) -> bag of X means
:: POLYNOM7:def 5
m.it <> 0.L or Support m = {} & it = EmptyBag X;
end;
definition
let X be set, L be non empty ZeroStr, m be Monomial of X,L;
func coefficient(m) -> Element of L equals
:: POLYNOM7:def 6
m.(term(m));
end;
theorem :: POLYNOM7:7
for X being set, L being non empty ZeroStr, m being Monomial of X
,L holds Support(m) = {} or Support(m) = {term(m)};
theorem :: POLYNOM7:8
for X being set, L being non empty ZeroStr, b being bag of X
holds coefficient(Monom(0.L,b)) = 0.L & term(Monom(0.L,b)) = EmptyBag X;
theorem :: POLYNOM7:9
for X being set, L being non empty ZeroStr, a being Element of L,
b being bag of X holds coefficient(Monom(a,b)) = a;
theorem :: POLYNOM7:10
for X being set, L being non trivial ZeroStr, a being non zero
Element of L, b being bag of X holds term(Monom(a,b)) = b;
theorem :: POLYNOM7:11
for X being set, L being non empty ZeroStr, m being Monomial of X,L
holds Monom(coefficient(m),term(m)) = m;
theorem :: POLYNOM7:12
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial doubleLoopStr, m
being Monomial of n,L, x being Function of n,L holds eval(m,x) = coefficient(m)
* eval(term(m),x);
theorem :: POLYNOM7:13
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial doubleLoopStr, a
being Element of L, b being bag of n, x being Function of n,L holds eval(Monom(
a,b),x) = a * eval(b,x);
begin :: Constant Polynomials
definition
let X be set, L be non empty ZeroStr, p be Series of X,L;
attr p is Constant means
:: POLYNOM7:def 7
for b being bag of X st b <> EmptyBag X holds p.b = 0.L;
end;
registration
let X be set, L be non empty ZeroStr;
cluster Constant for Series of X,L;
end;
definition
let X be set, L be non empty ZeroStr;
mode ConstPoly of X,L is Constant Series of X,L;
end;
registration
let X be set, L be non empty ZeroStr;
cluster Constant -> monomial-like for Series of X,L;
end;
theorem :: POLYNOM7:14
for X being set, L being non empty ZeroStr, p being Series of X,
L holds p is ConstPoly of X,L iff (p = 0_(X,L) or Support p = {EmptyBag X});
registration
let X be set, L be non empty ZeroStr;
cluster 0_(X,L) -> Constant;
end;
registration
let X be set, L be well-unital non empty doubleLoopStr;
cluster 1_(X,L) -> Constant;
end;
theorem :: POLYNOM7:15
for X being set, L being non empty ZeroStr, c being ConstPoly of
X,L holds Support(c) = {} or Support(c) = {EmptyBag X};
theorem :: POLYNOM7:16
for X being set, L being non empty ZeroStr, c being ConstPoly of X,L
holds term(c) = EmptyBag X & coefficient(c) = c.(EmptyBag X);
definition
let X be set, L be non empty ZeroStr, a be Element of L;
func a |(X,L) -> Series of X,L equals
:: POLYNOM7:def 8
0_(X,L)+*(EmptyBag X,a);
end;
registration
let X be set, L be non empty ZeroStr, a be Element of L;
cluster a |(X,L) -> Constant;
end;
theorem :: POLYNOM7:17
for X being set, L being non empty ZeroStr, p being Series of X,L
holds p is ConstPoly of X,L iff ex a being Element of L st p = a |(X,L);
theorem :: POLYNOM7:18
for X being set, L being non empty multLoopStr_0, a being
Element of L holds (a |(X,L)).EmptyBag X = a & for b being bag of X st b <>
EmptyBag X holds (a |(X,L)).b = 0.L;
theorem :: POLYNOM7:19
for X being set, L being non empty ZeroStr holds 0.L |(X,L) = 0_(X,L);
theorem :: POLYNOM7:20
for X being set, L being well-unital non empty multLoopStr_0 holds (
1.L) |(X,L) = 1_(X,L);
theorem :: POLYNOM7:21
for X being set, L being non empty ZeroStr, a,b being Element of L
holds a |(X,L) = b |(X,L) iff a = b;
theorem :: POLYNOM7:22
for X being set, L being non empty ZeroStr, a being Element of L holds
Support(a |(X,L)) = {} or Support(a |(X,L)) = {EmptyBag X};
theorem :: POLYNOM7:23
for X being set, L being non empty ZeroStr, a being Element of L
holds term(a |(X,L)) = EmptyBag X & coefficient(a |(X,L)) = a;
theorem :: POLYNOM7:24
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial doubleLoopStr, c
being ConstPoly of n,L, x being Function of n,L holds eval(c,x) = coefficient(c
);
theorem :: POLYNOM7:25
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial doubleLoopStr, a
being Element of L, x being Function of n,L holds eval(a |(n,L),x) = a;
begin :: Multiplication with Coefficients
definition
let X be set, L be non empty multLoopStr_0, p be Series of X,L, a be Element
of L;
func a * p -> Series of X,L means
:: POLYNOM7:def 9
for b being bag of X holds it.b = a * p.b;
func p * a -> Series of X,L means
:: POLYNOM7:def 10
for b being bag of X holds it.b = p.b * a;
end;
registration
let X be set, L be left_zeroed right_zeroed add-cancelable distributive non
empty doubleLoopStr, p be finite-Support Series of X,L, a be Element of L;
cluster a * p -> finite-Support;
cluster p * a -> finite-Support;
end;
theorem :: POLYNOM7:26
for X being set, L being commutative non empty multLoopStr_0, p
being Series of X,L, a being Element of L holds a * p = p * a;
theorem :: POLYNOM7:27
for n being Ordinal, L being add-associative
right_complementable right_zeroed left-distributive non empty doubleLoopStr,
p being Series of n,L, a being Element of L holds a * p = a |(n,L) *' p;
theorem :: POLYNOM7:28
for n being Ordinal, L being add-associative
right_complementable right_zeroed right-distributive non empty doubleLoopStr,
p being Series of n,L, a being Element of L holds p * a = p *' (a |(n,L));
theorem :: POLYNOM7:29
for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval(a*p,x) = a * eval(p,x);
theorem :: POLYNOM7:30
for n being Ordinal, L being left_zeroed right_zeroed
left_add-cancelable add-associative right_complementable well-unital
associative domRing-like distributive non trivial doubleLoopStr, p being
Polynomial of n,L, a being Element of L, x being Function of n,L holds eval(a*p
,x) = a * eval(p,x);
theorem :: POLYNOM7:31
for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval(p*a,x) = eval(p,x) * a;
theorem :: POLYNOM7:32
for n being Ordinal, L being left_zeroed right_zeroed
left_add-cancelable add-associative right_complementable well-unital
associative commutative distributive domRing-like non trivial doubleLoopStr,
p being Polynomial of n,L, a being Element of L, x being Function of n,L holds
eval(p*a,x) = eval(p,x) * a;
theorem :: POLYNOM7:33
for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval((a |(n,L))*'p,x) = a * eval(p,
x);
theorem :: POLYNOM7:34
for n being Ordinal, L being Abelian left_zeroed right_zeroed
add-associative right_complementable well-unital associative commutative
distributive non trivial doubleLoopStr, p being Polynomial of n,L, a being
Element of L, x being Function of n,L holds eval(p*'(a |(n,L)),x) = eval(p,x) *
a;