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