src/HOL/Algebra/Group.thy
changeset 19981 c0f124a0d385
parent 19931 fb32b43e7f80
child 19984 29bb4659f80a
--- a/src/HOL/Algebra/Group.thy	Mon Jul 03 20:03:11 2006 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Jul 04 11:35:49 2006 +0200
@@ -90,6 +90,14 @@
    apply (fast intro: inv_unique, fast)
   done
 
+lemma (in monoid) Units_l_inv_ex:
+  "x \<in> Units G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
+  by (unfold Units_def) auto
+
+lemma (in monoid) Units_r_inv_ex:
+  "x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
+  by (unfold Units_def) auto
+
 lemma (in monoid) Units_l_inv:
   "x \<in> Units G ==> inv x \<otimes> x = \<one>"
   apply (unfold Units_def m_inv_def, auto)
@@ -271,6 +279,14 @@
   "x \<in> carrier G ==> inv x \<in> carrier G"
   using Units_inv_closed by simp
 
+lemma (in group) l_inv_ex [simp]:
+  "x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
+  using Units_l_inv_ex by simp
+
+lemma (in group) r_inv_ex [simp]:
+  "x \<in> carrier G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
+  using Units_r_inv_ex by simp
+
 lemma (in group) l_inv [simp]:
   "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
   using Units_l_inv by simp