src/HOL/Algebra/abstract/RingHomo.thy

Algebra and Polynomial theories, by Clemens Ballarin

(*
    Ring homomorphism
    $Id$
    Author: Clemens Ballarin, started 15 April 1997
*)

RingHomo = NatSum +

consts
  homo	:: ('a::ringS => 'b::ringS) => bool

defs
  homo_def	"homo f == (ALL a b. f (a + b) = f a + f b &
			      f (a * b) = f a * f b) &
			   f <1> = <1>"

end