src/HOL/Algebra/abstract/RingHomo.thy
author wenzelm
Sat Sep 17 20:49:14 2005 +0200 (2005-09-17)
changeset 17479 68a7acb5f22e
parent 13735 7de9342aca7a
child 20318 0e0ea63fe768
permissions -rw-r--r--
converted to Isar theory format;
paulson@7998
     1
(*
paulson@7998
     2
    Ring homomorphism
paulson@7998
     3
    $Id$
paulson@7998
     4
    Author: Clemens Ballarin, started 15 April 1997
paulson@7998
     5
*)
paulson@7998
     6
wenzelm@17479
     7
theory RingHomo imports Ring begin
paulson@7998
     8
wenzelm@17479
     9
constdefs
wenzelm@17479
    10
  homo  :: "('a::ring => 'b::ring) => bool"
wenzelm@17479
    11
  "homo f == (ALL a b. f (a + b) = f a + f b &
wenzelm@17479
    12
                                   f (a * b) = f a * f b) &
wenzelm@17479
    13
                                   f 1 = 1"
paulson@7998
    14
paulson@7998
    15
end