src/HOL/Algebra/Group.thy
 changeset 19981 c0f124a0d385 parent 19931 fb32b43e7f80 child 19984 29bb4659f80a
```     1.1 --- a/src/HOL/Algebra/Group.thy	Mon Jul 03 20:03:11 2006 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jul 04 11:35:49 2006 +0200
1.3 @@ -90,6 +90,14 @@
1.4     apply (fast intro: inv_unique, fast)
1.5    done
1.6
1.7 +lemma (in monoid) Units_l_inv_ex:
1.8 +  "x \<in> Units G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
1.9 +  by (unfold Units_def) auto
1.10 +
1.11 +lemma (in monoid) Units_r_inv_ex:
1.12 +  "x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
1.13 +  by (unfold Units_def) auto
1.14 +
1.15  lemma (in monoid) Units_l_inv:
1.16    "x \<in> Units G ==> inv x \<otimes> x = \<one>"
1.17    apply (unfold Units_def m_inv_def, auto)
1.18 @@ -271,6 +279,14 @@
1.19    "x \<in> carrier G ==> inv x \<in> carrier G"
1.20    using Units_inv_closed by simp
1.21
1.22 +lemma (in group) l_inv_ex [simp]:
1.23 +  "x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
1.24 +  using Units_l_inv_ex by simp
1.25 +
1.26 +lemma (in group) r_inv_ex [simp]:
1.27 +  "x \<in> carrier G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
1.28 +  using Units_r_inv_ex by simp
1.29 +
1.30  lemma (in group) l_inv [simp]:
1.31    "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
1.32    using Units_l_inv by simp
```