The abstract of the Mizar article:

The Evaluation of Polynomials

by

Robert Milewski

Received June 7, 2000

MML identifier: POLYNOM4

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM_1, FINSEQ_1, RELAT_1, FUNCT_1, RFINSEQ, RLVECT_1, FINSEQ_2,
      BINOP_1, VECTSP_1, LATTICES, REALSET1, ALGSTR_2, NORMSP_1, POLYNOM3,
      ARYTM_3, ALGSEQ_1, POLYNOM1, FUNCOP_1, SQUARE_1, FINSEQ_4, FUNCT_4,
      GROUP_1, POLYNOM2, VECTSP_2, PRE_TOPC, ENDALG, GRCAT_1, COHSP_1,
      QUOFIELD, POLYNOM4, ALGSTR_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, STRUCT_0,
      NAT_1, SQUARE_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FINSEQ_1, FINSEQ_2,
      FINSEQ_4, FINSOP_1, RFINSEQ, TOPREAL1, BINARITH, PRE_TOPC, NORMSP_1,
      RLVECT_1, VECTSP_1, VECTSP_2, FVSUM_1, REALSET1, GROUP_1, ALGSTR_1,
      GRCAT_1, ENDALG, QUOFIELD, POLYNOM1, ALGSEQ_1, POLYNOM3;
 constructors REAL_1, SQUARE_1, FINSOP_1, SETWOP_2, RFINSEQ, TOPREAL1,
      BINARITH, QUOFIELD, FVSUM_1, ALGSTR_2, ALGSEQ_1, GRCAT_1, ENDALG,
      POLYNOM1, POLYNOM3, FINSEQOP, ALGSTR_1, MEMBERED;
 clusters STRUCT_0, RELSET_1, ALGSTR_1, FINSEQ_1, FINSEQ_2, VECTSP_2, VECTSP_1,
      POLYNOM1, POLYNOM3, INT_1, MONOID_0, XREAL_0, MEMBERED, ORDINAL2, GCD_1;
 requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;


begin  :: Preliminaries

  theorem :: POLYNOM4:1
   for n be Nat holds 0-'n = 0;

canceled;

  theorem :: POLYNOM4:3
   for D be non empty set
   for p be FinSequence of D
   for n be Nat st 1 <= n & n <= len p holds
    p = (p|(n-'1))^<*p.n*>^(p/^n);

definition
cluster Field-like -> domRing-like
           (left_zeroed add-right-cancelable right-distributive
            left_unital commutative associative (non empty doubleLoopStr));
end;

definition
 cluster strict Abelian add-associative right_zeroed right_complementable
         associative commutative distributive well-unital
         domRing-like Field-like
         non degenerated non trivial (non empty doubleLoopStr);
end;

begin  :: About Polynomials

canceled;

  theorem :: POLYNOM4:5
   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:6
   for L be non empty ZeroStr holds
    len 0_.(L) = 0;

  theorem :: POLYNOM4:7
   for L be non degenerated (non empty multLoopStr_0) holds
    len 1_.(L) = 1;

  theorem :: POLYNOM4:8
   for L be non empty ZeroStr
   for p be Polynomial of L st len p = 0 holds
    p = 0_.(L);

  theorem :: POLYNOM4:9
   for L be right_zeroed (non empty LoopStr)
   for p,q be Polynomial of L
   for n be 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
    (non empty LoopStr)
   for p,q be Polynomial of L st len p <> len q holds
    len (p+q) = max(len p,len q);

  theorem :: POLYNOM4:11
   for L be add-associative right_zeroed right_complementable
    (non empty LoopStr)
   for p be Polynomial of L holds
    len (-p) = len p;

  theorem :: POLYNOM4:12
     for L be add-associative right_zeroed right_complementable
    (non empty LoopStr)
   for p,q be Polynomial of L
   for n be Nat st n >= len p & n >= len q holds
    n >= len (p-q);

  theorem :: POLYNOM4:13
for L be add-associative right_zeroed right_complementable distributive
         commutative 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 Nat st n <> len p-'1 holds it.n = 0.L;
  end;

  theorem :: POLYNOM4:14
   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));

  definition
   let L be non empty ZeroStr;
   let p be Polynomial of L;
   cluster Leading-Monomial(p) -> finite-Support;
  end;

  theorem :: POLYNOM4:15
   for L be non empty ZeroStr
   for p be Polynomial of L st len p = 0 holds
    Leading-Monomial(p) = 0_.(L);

  theorem :: POLYNOM4:16
     for L be non empty ZeroStr holds
    Leading-Monomial(0_.(L)) = 0_.(L);

  theorem :: POLYNOM4:17
     for L be non degenerated (non empty multLoopStr_0) holds
    Leading-Monomial(1_.(L)) = 1_.(L);

  theorem :: POLYNOM4:18
   for L be non empty ZeroStr
   for p be Polynomial of L holds
    len Leading-Monomial(p) = len p;

  theorem :: POLYNOM4:19
   for L be add-associative right_zeroed right_complementable
    (non empty LoopStr)
   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 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 the carrier 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 Nat st n in dom F holds F.n = p.(n-'1) * (power L).(x,n-'1);
  end;

  theorem :: POLYNOM4:20
   for L be unital (non empty doubleLoopStr)
   for x be Element of the carrier of L holds
    eval(0_.(L),x) = 0.L;

  theorem :: POLYNOM4:21
   for L be well-unital add-associative right_zeroed right_complementable
    associative non degenerated (non empty doubleLoopStr)
   for x be Element of the carrier of L holds
    eval(1_.(L),x) = 1_(L);

  theorem :: POLYNOM4:22
   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 the carrier of L holds
    eval(p+q,x) = eval(p,x) + eval(q,x);

  theorem :: POLYNOM4:23
   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 the carrier of L holds
    eval(-p,x) = -eval(p,x);

  theorem :: POLYNOM4:24
     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 the carrier of L holds
    eval(p-q,x) = eval(p,x) - eval(q,x);

  theorem :: POLYNOM4:25
   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 the carrier of L holds
    eval(Leading-Monomial(p),x) = p.(len p-'1) * (power L).(x,len p-'1);

  theorem :: POLYNOM4:26
   for L be add-associative right_zeroed right_complementable Abelian
    left_unital distributive commutative associative non trivial
    (non empty doubleLoopStr)
   for p,q be Polynomial of L
   for x be Element of the carrier of L holds
    eval((Leading-Monomial(p))*'q,x) = eval(Leading-Monomial(p),x) * eval(q,x);

  theorem :: POLYNOM4:27
   for L be add-associative right_zeroed right_complementable Abelian
    left_unital distributive commutative associative non trivial
    (non empty doubleLoopStr)
   for p,q be Polynomial of L
   for x be Element of the carrier 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 the carrier of L;
   func Polynom-Evaluation(L,x) -> map of Polynom-Ring L,L means
:: POLYNOM4:def 3
    for p be Polynomial of L holds it.p = eval(p,x);
  end;

  definition
   let L be add-associative right_zeroed right_complementable distributive
    associative well-unital non degenerated (non empty doubleLoopStr);
   let x be Element of the carrier of L;
   cluster Polynom-Evaluation(L,x) -> unity-preserving;
  end;

  definition
   let L be Abelian add-associative right_zeroed right_complementable
    distributive unital (non empty doubleLoopStr);
   let x be Element of the carrier of L;
   cluster Polynom-Evaluation(L,x) -> additive;
  end;

  definition
   let L be add-associative right_zeroed right_complementable Abelian
    left_unital distributive commutative associative non trivial
    (non empty doubleLoopStr);
   let x be Element of the carrier of L;
   cluster Polynom-Evaluation(L,x) -> multiplicative;
  end;

  definition
   let L be add-associative right_zeroed right_complementable Abelian
    left_unital distributive commutative associative non degenerated
    (non empty doubleLoopStr);
   let x be Element of the carrier of L;
   cluster Polynom-Evaluation(L,x) -> RingHomomorphism;
  end;