:: Evaluation of Polynomials :: by Robert Milewski :: :: Received June 7, 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, XBOOLE_0, FINSEQ_1, SUBSET_1, XXREAL_0, RELAT_1, ARYTM_1, ORDINAL4, FUNCT_1, RFINSEQ, ALGSTR_1, ALGSTR_0, VECTSP_1, SUPINF_2, ARYTM_3, VECTSP_2, BINOP_1, MESFUNC1, STRUCT_0, RLVECT_1, LATTICES, GROUP_1, ZFMISC_1, NAT_1, POLYNOM3, CARD_3, CARD_1, ALGSEQ_1, POLYNOM1, TARSKI, PARTFUN1, FUNCT_4, POLYNOM2, FINSEQ_2, MSSUBFAM, QUOFIELD, POLYNOM4; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_1, NAT_1, STRUCT_0, ALGSTR_0, FINSEQ_2, FUNCT_7, RFINSEQ, NAT_D, RLVECT_1, VFUNCT_1, GROUP_1, VECTSP_1, VECTSP_2, NORMSP_1, FVSUM_1, ALGSTR_1, GRCAT_1, QUOFIELD, ALGSEQ_1, POLYNOM3, GROUP_6, XXREAL_0; constructors FINSEQOP, RFINSEQ, NAT_D, ALGSEQ_1, GRCAT_1, GROUP_6, QUOFIELD, POLYNOM3, REAL_1, ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1, RINGCAT1; registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM3, ALGSTR_0, CARD_1, VFUNCT_1, FUNCT_2, RINGCAT1; requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM; begin theorem :: POLYNOM4:1 for D be non empty set for p be FinSequence of D for n be Element of NAT st 1 <= n & n <= len p holds p = (p|(n-'1))^<*p.n*>^(p/^n); registration cluster almost_left_invertible -> domRing-like for left_zeroed right_add-cancelable right-distributive well-unital associative non empty doubleLoopStr; end; registration cluster strict Abelian add-associative right_zeroed right_complementable associative commutative distributive unital domRing-like almost_left_invertible non degenerated for non empty doubleLoopStr; end; begin :: About Polynomials theorem :: POLYNOM4:2 for L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr for p be sequence of L holds (0_.(L ))*'p = 0_.(L); theorem :: POLYNOM4:3 for L be non empty ZeroStr holds len 0_.(L) = 0; theorem :: POLYNOM4:4 for L be non degenerated non empty multLoopStr_0 holds len 1_.( L) = 1; theorem :: POLYNOM4:5 for L be non empty ZeroStr for p be Polynomial of L st len p = 0 holds p = 0_.(L); theorem :: POLYNOM4:6 for L be right_zeroed non empty addLoopStr for p,q be Polynomial of L for n be Element of NAT st n >= len p & n >= len q holds n >= len (p+q); theorem :: POLYNOM4:7 for L be add-associative right_zeroed right_complementable non empty addLoopStr for p,q be Polynomial of L st len p <> len q holds len (p+q) = max(len p,len q); theorem :: POLYNOM4:8 for L be add-associative right_zeroed right_complementable non empty addLoopStr for p be Polynomial of L holds len (-p) = len p; theorem :: POLYNOM4:9 for L be add-associative right_zeroed right_complementable non empty addLoopStr for p,q be Polynomial of L for n be Element of NAT st n >= len p & n >= len q holds n >= len (p-q); theorem :: POLYNOM4:10 for L be add-associative right_zeroed right_complementable distributive associative left_unital non empty doubleLoopStr, p,q be Polynomial of L st p.(len p -'1) * q.(len q -'1) <> 0.L holds len (p*'q) = len p + len q - 1; begin :: Leading Monomials definition let L be non empty ZeroStr; let p be Polynomial of L; func Leading-Monomial(p) -> sequence of L means :: POLYNOM4:def 1 it.(len p-'1) = p.( len p-'1) & for n be Element of NAT st n <> len p-'1 holds it.n = 0.L; end; theorem :: POLYNOM4:11 for L be non empty ZeroStr for p be Polynomial of L holds Leading-Monomial(p) = 0_.(L)+*(len p-'1,p.(len p-'1)); registration let L be non empty ZeroStr; let p be Polynomial of L; cluster Leading-Monomial(p) -> finite-Support; end; theorem :: POLYNOM4:12 for L be non empty ZeroStr for p be Polynomial of L st len p = 0 holds Leading-Monomial(p) = 0_.(L); theorem :: POLYNOM4:13 for L be non empty ZeroStr holds Leading-Monomial(0_.(L)) = 0_.(L); theorem :: POLYNOM4:14 for L be non degenerated non empty multLoopStr_0 holds Leading-Monomial(1_.(L)) = 1_.(L); theorem :: POLYNOM4:15 for L be non empty ZeroStr for p be Polynomial of L holds len Leading-Monomial(p) = len p; theorem :: POLYNOM4:16 for L be add-associative right_zeroed right_complementable non empty addLoopStr for p be Polynomial of L st len p <> 0 ex q be Polynomial of L st len q < len p & p = q+Leading-Monomial(p) & for n be Element of NAT st n < len p-1 holds q.n = p.n; begin :: Evaluation of Polynomials definition let L be unital non empty doubleLoopStr; let p be Polynomial of L; let x be Element of L; func eval(p,x) -> Element of L means :: POLYNOM4:def 2 ex F be FinSequence of the carrier of L st it = Sum F & len F = len p & for n be Element of NAT st n in dom F holds F.n = p.(n-'1) * (power L).(x,n-'1); end; theorem :: POLYNOM4:17 for L be unital non empty doubleLoopStr for x be Element of L holds eval(0_.(L),x) = 0.L; theorem :: POLYNOM4:18 for L be well-unital add-associative right_zeroed right_complementable associative non degenerated non empty doubleLoopStr for x be Element of L holds eval(1_.(L),x) = 1.L; theorem :: POLYNOM4:19 for L be Abelian add-associative right_zeroed right_complementable unital left-distributive non empty doubleLoopStr for p,q be Polynomial of L for x be Element of L holds eval(p+q,x) = eval(p,x) + eval(q ,x); theorem :: POLYNOM4:20 for L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr for p be Polynomial of L for x be Element of L holds eval(-p,x) = -eval(p,x); theorem :: POLYNOM4:21 for L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr for p,q be Polynomial of L for x be Element of L holds eval(p-q,x) = eval(p,x) - eval(q,x); theorem :: POLYNOM4:22 for L be add-associative right_zeroed right_complementable right_zeroed distributive unital non empty doubleLoopStr for p be Polynomial of L for x be Element of L holds eval(Leading-Monomial(p),x) = p.(len p-'1) * ( power L).(x,len p-'1); theorem :: POLYNOM4:23 for L be add-associative right_zeroed right_complementable Abelian left_unital distributive commutative associative non trivial doubleLoopStr for p,q be Polynomial of L for x be Element of L holds eval(( Leading-Monomial(p))*'q,x) = eval(Leading-Monomial(p),x) * eval(q,x); theorem :: POLYNOM4:24 for L be add-associative right_zeroed right_complementable Abelian left_unital distributive commutative associative non trivial doubleLoopStr for p,q be Polynomial of L for x be Element of L holds eval(p*'q ,x) = eval(p,x) * eval(q,x); begin :: Evaluation Homomorphism definition let L be add-associative right_zeroed right_complementable distributive unital non empty doubleLoopStr; let x be Element of L; func Polynom-Evaluation(L,x) -> Function of Polynom-Ring L,L means :: POLYNOM4:def 3 for p be Polynomial of L holds it.p = eval(p,x); end; registration let L be add-associative right_zeroed right_complementable distributive associative well-unital non degenerated Abelian non empty doubleLoopStr; let x be Element of L; cluster Polynom-Evaluation(L,x) -> unity-preserving; end; registration let L be Abelian add-associative right_zeroed right_complementable distributive unital non empty doubleLoopStr; let x be Element of L; cluster Polynom-Evaluation(L,x) -> additive; end; registration let L be add-associative right_zeroed right_complementable Abelian left_unital distributive commutative associative non trivial doubleLoopStr; let x be Element of L; cluster Polynom-Evaluation(L,x) -> multiplicative; end; registration let L be add-associative right_zeroed right_complementable Abelian well-unital distributive commutative associative non degenerated doubleLoopStr; let x be Element of L; cluster Polynom-Evaluation(L,x) -> RingHomomorphism; end;