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 theory RingHomo imports Ring begin |
7 theory RingHomo imports Ring2 begin |
8 |
8 |
9 constdefs |
9 constdefs |
10 homo :: "('a::ring => 'b::ring) => bool" |
10 homo :: "('a::ring => 'b::ring) => bool" |
11 "homo f == (ALL a b. f (a + b) = f a + f b & |
11 "homo f == (ALL a b. f (a + b) = f a + f b & |
12 f (a * b) = f a * f b) & |
12 f (a * b) = f a * f b) & |