2 Ideals for commutative rings |
2 Ideals for commutative rings |
3 $Id$ |
3 $Id$ |
4 Author: Clemens Ballarin, started 24 September 1999 |
4 Author: Clemens Ballarin, started 24 September 1999 |
5 *) |
5 *) |
6 |
6 |
7 Ideal = Ring + |
7 theory Ideal imports Ring begin |
8 |
8 |
9 consts |
9 consts |
10 ideal_of :: ('a::ring) set => 'a set |
10 ideal_of :: "('a::ring) set => 'a set" |
11 is_ideal :: ('a::ring) set => bool |
11 is_ideal :: "('a::ring) set => bool" |
12 is_pideal :: ('a::ring) set => bool |
12 is_pideal :: "('a::ring) set => bool" |
13 |
13 |
14 defs |
14 defs |
15 is_ideal_def "is_ideal I == (ALL a: I. ALL b: I. a + b : I) & |
15 is_ideal_def: "is_ideal I == (ALL a: I. ALL b: I. a + b : I) & |
16 (ALL a: I. - a : I) & 0 : I & |
16 (ALL a: I. - a : I) & 0 : I & |
17 (ALL a: I. ALL r. a * r : I)" |
17 (ALL a: I. ALL r. a * r : I)" |
18 ideal_of_def "ideal_of S == Inter {I. is_ideal I & S <= I}" |
18 ideal_of_def: "ideal_of S == Inter {I. is_ideal I & S <= I}" |
19 is_pideal_def "is_pideal I == (EX a. I = ideal_of {a})" |
19 is_pideal_def: "is_pideal I == (EX a. I = ideal_of {a})" |
20 |
20 |
21 (* Principle ideal domains *) |
21 text {* Principle ideal domains *} |
22 |
22 |
23 axclass |
23 axclass pid < "domain" |
24 pid < domain |
24 pid_ax: "is_ideal I ==> is_pideal I" |
25 |
|
26 pid_ax "is_ideal I ==> is_pideal I" |
|
27 |
25 |
28 end |
26 end |