equal
deleted
inserted
replaced
113 (%x. a \<otimes> x) ` (carrier G) = (carrier G)" |
113 (%x. a \<otimes> x) ` (carrier G) = (carrier G)" |
114 apply (auto simp add: image_def) |
114 apply (auto simp add: image_def) |
115 apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI) |
115 apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI) |
116 apply auto |
116 apply auto |
117 (* auto should get this. I suppose we need "comm_monoid_simprules" |
117 (* auto should get this. I suppose we need "comm_monoid_simprules" |
118 for mult_ac rewriting. *) |
118 for ac_simps rewriting. *) |
119 apply (subst m_assoc [symmetric]) |
119 apply (subst m_assoc [symmetric]) |
120 apply auto |
120 apply auto |
121 done |
121 done |
122 |
122 |
123 lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> |
123 lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> |