isabelle: src/HOL/Algebra/abstract/RingHomo.thy@d2b071e65e4c (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	Ring homomorphism
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: 7998 diff changeset	7	RingHomo = Ring +
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: 7998 diff changeset	10	homo :: ('a::ring => 'b::ring) => bool
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12	defs
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13	homo_def "homo f == (ALL a b. f (a + b) = f a + f b &
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14	f (a * b) = f a * f b) &
13735 7de9342aca7a HOL-Algebra partially ported to Isar. ballarin parents: 7998 diff changeset	15	f 1 = 1"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	16
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	17	end

author	wenzelm
	Fri, 21 May 2004 21:15:10 +0200
changeset 14767	d2b071e65e4c
parent 13735	7de9342aca7a
child 17479	68a7acb5f22e
permissions	-rw-r--r--