isabelle: src/HOL/Algebra/abstract/RingHomo.thy@fc385ce6187d (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
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	7	theory RingHomo imports Ring begin
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	8
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	9	constdefs
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	10	homo :: "('a::ring => 'b::ring) => bool"
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	11	"homo f == (ALL a b. f (a + b) = f a + f b &
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	12	f (a * b) = f a * f b) &
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	13	f 1 = 1"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15	end

author	aspinall
	Fri, 30 Sep 2005 18:18:34 +0200
changeset 17740	fc385ce6187d
parent 17479	68a7acb5f22e
child 20318	0e0ea63fe768
permissions	-rw-r--r--