src/HOL/Algebra/poly/PolyHomo.thy
author kleing
Tue, 13 May 2003 08:59:21 +0200
changeset 14024 213dcc39358f
parent 13936 d3671b878828
child 17479 68a7acb5f22e
permissions -rw-r--r--
HOL-Real -> HOL-Complex

(*
    Universal property and evaluation homomorphism of univariate polynomials
    $Id$
    Author: Clemens Ballarin, started 15 April 1997
*)

PolyHomo = UnivPoly2 +

consts
  EVAL2	:: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
  EVAL	:: "['a::ring, 'a up] => 'a"

defs
  EVAL2_def	"EVAL2 phi a p ==
                 setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
  EVAL_def	"EVAL == EVAL2 (%x. x)"

end