src/HOL/Algebra/Group.thy
changeset 19984 29bb4659f80a
parent 19981 c0f124a0d385
child 20318 0e0ea63fe768
equal deleted inserted replaced
19983:d649506f40c3 19984:29bb4659f80a
   656 
   656 
   657 lemma (in group) group_comm_groupI:
   657 lemma (in group) group_comm_groupI:
   658   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
   658   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
   659       x \<otimes> y = y \<otimes> x"
   659       x \<otimes> y = y \<otimes> x"
   660   shows "comm_group G"
   660   shows "comm_group G"
   661   by intro_locales (simp_all add: m_comm)
   661   by unfold_locales (simp_all add: m_comm)
   662 
   662 
   663 lemma comm_groupI:
   663 lemma comm_groupI:
   664   fixes G (structure)
   664   fixes G (structure)
   665   assumes m_closed:
   665   assumes m_closed:
   666       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
   666       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"