equal
deleted
inserted
replaced
11 is_ideal :: ('a::ringS) set => bool |
11 is_ideal :: ('a::ringS) set => bool |
12 is_pideal :: ('a::ringS) set => bool |
12 is_pideal :: ('a::ringS) 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 (* Principle ideal domains *) |