equal
deleted
inserted
replaced
2 Ring homomorphism |
2 Ring homomorphism |
3 $Id$ |
3 $Id$ |
4 Author: Clemens Ballarin, started 15 April 1997 |
4 Author: Clemens Ballarin, started 15 April 1997 |
5 *) |
5 *) |
6 |
6 |
7 RingHomo = NatSum + |
7 RingHomo = Ring + |
8 |
8 |
9 consts |
9 consts |
10 homo :: ('a::ringS => 'b::ringS) => bool |
10 homo :: ('a::ring => 'b::ring) => bool |
11 |
11 |
12 defs |
12 defs |
13 homo_def "homo f == (ALL a b. f (a + b) = f a + f b & |
13 homo_def "homo f == (ALL a b. f (a + b) = f a + f b & |
14 f (a * b) = f a * f b) & |
14 f (a * b) = f a * f b) & |
15 f <1> = <1>" |
15 f 1 = 1" |
16 |
16 |
17 end |
17 end |