isabelle: src/HOL/Algebra/poly/PolyHomo.thy@8e739a6eaf11 (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
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13735 diff changeset	7	PolyHomo = UnivPoly2 +
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	obua
	Sun, 09 May 2004 23:04:36 +0200
changeset 14722	8e739a6eaf11
parent 13936	d3671b878828
child 17479	68a7acb5f22e
permissions	-rw-r--r--