equal
deleted
inserted
replaced
710 lemma (in abelian_subgroup) a_repr_independenceD: |
710 lemma (in abelian_subgroup) a_repr_independenceD: |
711 assumes ycarr: "y \<in> carrier G" |
711 assumes ycarr: "y \<in> carrier G" |
712 and repr: "H +> x = H +> y" |
712 and repr: "H +> x = H +> y" |
713 shows "y \<in> H +> x" |
713 shows "y \<in> H +> x" |
714 by (rule group.repr_independenceD [OF a_group a_subgroup, |
714 by (rule group.repr_independenceD [OF a_group a_subgroup, |
715 folded a_r_coset_def, simplified monoid_record_simps]) |
715 folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr) |
716 |
716 |
717 |
717 |
718 subsection {* Lemmas for the Set of Right Cosets *} |
718 subsection {* Lemmas for the Set of Right Cosets *} |
719 |
719 |
720 lemma (in abelian_subgroup) a_rcosets_carrier: |
720 lemma (in abelian_subgroup) a_rcosets_carrier: |
729 lemma (in abelian_monoid) set_add_closed: |
729 lemma (in abelian_monoid) set_add_closed: |
730 assumes Acarr: "A \<subseteq> carrier G" |
730 assumes Acarr: "A \<subseteq> carrier G" |
731 and Bcarr: "B \<subseteq> carrier G" |
731 and Bcarr: "B \<subseteq> carrier G" |
732 shows "A <+> B \<subseteq> carrier G" |
732 shows "A <+> B \<subseteq> carrier G" |
733 by (rule monoid.set_mult_closed [OF a_monoid, |
733 by (rule monoid.set_mult_closed [OF a_monoid, |
734 folded set_add_def, simplified monoid_record_simps]) |
734 folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr) |
735 |
735 |
736 lemma (in abelian_group) add_additive_subgroups: |
736 lemma (in abelian_group) add_additive_subgroups: |
737 assumes subH: "additive_subgroup H G" |
737 assumes subH: "additive_subgroup H G" |
738 and subK: "additive_subgroup K G" |
738 and subK: "additive_subgroup K G" |
739 shows "additive_subgroup (H <+> K) G" |
739 shows "additive_subgroup (H <+> K) G" |