equal
deleted
inserted
replaced
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Ring axioms *} |
13 subsection {* Ring axioms *} |
14 |
14 |
15 class ring = zero + one + plus + minus + uminus + times + inverse + recpower + Ring_and_Field.dvd + |
15 class ring = zero + one + plus + minus + uminus + times + inverse + power + dvd + |
16 assumes a_assoc: "(a + b) + c = a + (b + c)" |
16 assumes a_assoc: "(a + b) + c = a + (b + c)" |
17 and l_zero: "0 + a = a" |
17 and l_zero: "0 + a = a" |
18 and l_neg: "(-a) + a = 0" |
18 and l_neg: "(-a) + a = 0" |
19 and a_comm: "a + b = b + a" |
19 and a_comm: "a + b = b + a" |
20 |
20 |