:: Evaluation of Polynomials
:: by Robert Milewski
::
:: Received June 7, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: POLYNOM4:1
canceled;
theorem :: POLYNOM4:2
canceled;
theorem :: POLYNOM4:3
Lm1:
for R being non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr
for a being Element of R holds a * (0. R) = 0. R
theorem :: POLYNOM4:4
canceled;
theorem Th5: :: POLYNOM4:5
theorem Th6: :: POLYNOM4:6
theorem Th7: :: POLYNOM4:7
theorem Th8: :: POLYNOM4:8
theorem Th9: :: POLYNOM4:9
theorem Th10: :: POLYNOM4:10
theorem Th11: :: POLYNOM4:11
theorem :: POLYNOM4:12
theorem :: POLYNOM4:13
:: deftheorem Def1 defines Leading-Monomial POLYNOM4:def 1 :
theorem Th14: :: POLYNOM4:14
theorem Th15: :: POLYNOM4:15
theorem :: POLYNOM4:16
theorem :: POLYNOM4:17
theorem Th18: :: POLYNOM4:18
theorem Th19: :: POLYNOM4:19
:: deftheorem Def2 defines eval POLYNOM4:def 2 :
theorem Th20: :: POLYNOM4:20
theorem Th21: :: POLYNOM4:21
Lm2:
for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for x being Element of F holds (0. F) * x = 0. F
theorem Th22: :: POLYNOM4:22
theorem Th23: :: POLYNOM4:23
theorem :: POLYNOM4:24
theorem Th25: :: POLYNOM4:25
Lm3:
for L being non empty right_complementable add-associative right_zeroed unital associative distributive doubleLoopStr
for p, q being Polynomial of L st len p > 0 & len q > 0 holds
for x being Element of L holds eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . x,(((len p) + (len q)) -' 2))
Lm4:
for L being non empty non trivial right_complementable add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr
for p, q being Polynomial of L
for x being Element of L holds eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = (eval (Leading-Monomial p),x) * (eval (Leading-Monomial q),x)
theorem Th26: :: POLYNOM4:26
theorem Th27: :: POLYNOM4:27
:: deftheorem Def3 defines Polynom-Evaluation POLYNOM4:def 3 :