src/HOL/Algebra/Group.thy
changeset 13944 9b34607cd83e
parent 13943 83d842ccd4aa
child 13949 0ce528cd6f19
     1.1 --- a/src/HOL/Algebra/Group.thy	Thu May 01 10:29:44 2003 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Thu May 01 11:54:18 2003 +0200
     1.3 @@ -348,7 +348,7 @@
     1.4    "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
     1.5    by (rule Units_inv_comm) auto                          
     1.6  
     1.7 -lemma (in group) m_inv_equality:
     1.8 +lemma (in group) inv_equality:
     1.9       "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
    1.10  apply (simp add: m_inv_def)
    1.11  apply (rule the_equality)
    1.12 @@ -567,6 +567,27 @@
    1.13      (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
    1.14        simp add: DirProdGroup_def DirProdSemigroup_def)
    1.15  
    1.16 +lemma carrier_DirProdGroup [simp]:
    1.17 +     "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
    1.18 +  by (simp add: DirProdGroup_def DirProdSemigroup_def)
    1.19 +
    1.20 +lemma one_DirProdGroup [simp]:
    1.21 +     "one (G \<times>\<^sub>g H) = (one G, one H)"
    1.22 +  by (simp add: DirProdGroup_def DirProdSemigroup_def);
    1.23 +
    1.24 +lemma mult_DirProdGroup [simp]:
    1.25 +     "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
    1.26 +  by (simp add: DirProdGroup_def DirProdSemigroup_def)
    1.27 +
    1.28 +lemma inv_DirProdGroup [simp]:
    1.29 +  includes group G + group H
    1.30 +  assumes g: "g \<in> carrier G"
    1.31 +      and h: "h \<in> carrier H"
    1.32 +  shows "m_inv (G \<times>\<^sub>g H) (g, h) = (m_inv G g, m_inv H h)"
    1.33 +  apply (rule group.inv_equality [OF DirProdGroup_group])
    1.34 +  apply (simp_all add: prems group_def group.l_inv)
    1.35 +  done
    1.36 +
    1.37  subsection {* Homomorphisms *}
    1.38  
    1.39  constdefs