equal
deleted
inserted
replaced
88 also have "... = a * 1" by (simp add: mult_commute) |
88 also have "... = a * 1" by (simp add: mult_commute) |
89 finally show ?thesis . |
89 finally show ?thesis . |
90 qed |
90 qed |
91 |
91 |
92 lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))" |
92 lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))" |
93 by(rule mk_left_commute[OF mult_assoc mult_commute]) |
93 by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute]) |
94 |
94 |
95 theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute |
95 theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute |
96 |
96 |
97 lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = 1" |
97 lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = 1" |
98 proof - |
98 proof - |