| author | wenzelm |
| Thu, 29 Apr 2004 06:02:48 +0200 | |
| changeset 14684 | d796124e435c |
| parent 13936 | d3671b878828 |
| child 17479 | 68a7acb5f22e |
| permissions | -rw-r--r-- |
(* 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