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```