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