equal
deleted
inserted
replaced
232 |
232 |
233 lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> [^] n" |
233 lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> [^] n" |
234 by (induct n) (simp_all add: m_ac) |
234 by (induct n) (simp_all add: m_ac) |
235 |
235 |
236 definition cring_class_ops :: "'a::comm_ring_1 ring" |
236 definition cring_class_ops :: "'a::comm_ring_1 ring" |
237 where "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>" |
237 where "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>" |
238 |
238 |
239 lemma cring_class: "cring cring_class_ops" |
239 lemma cring_class: "cring cring_class_ops" |
240 apply unfold_locales |
240 apply unfold_locales |
241 apply (auto simp add: cring_class_ops_def ring_distribs Units_def) |
241 apply (auto simp add: cring_class_ops_def ring_distribs Units_def) |
242 apply (rule_tac x="- x" in exI) |
242 apply (rule_tac x="- x" in exI) |