isabelle: src/HOL/Algebra/poly/PolyHomo.thy@7de9342aca7a (annotated)

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	(*
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	Universal property and evaluation homomorphism of univariate polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3	$Id$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	Author: Clemens Ballarin, started 15 April 1997
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	6
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11779 diff changeset	7	PolyHomo = UnivPoly +
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	8
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	9	consts
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11779 diff changeset	10	EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11779 diff changeset	11	EVAL :: "['a::ring, 'a up] => 'a"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13	defs
11093 62c2e0af1d30 Changes to HOL/Algebra: ballarin parents: 9279 diff changeset	14	EVAL2_def "EVAL2 phi a p ==
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 11779 diff changeset	15	setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	16	EVAL_def "EVAL == EVAL2 (%x. x)"
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	17
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	18	end

author	ballarin
	Thu, 28 Nov 2002 10:50:42 +0100
changeset 13735	7de9342aca7a
parent 11779	1aa328cb273a
child 13936	d3671b878828
permissions	-rw-r--r--