equal
deleted
inserted
replaced
105 apply (simp add: r_coset_def) |
105 apply (simp add: r_coset_def) |
106 apply (blast intro: sym l_one subgroup.subset [THEN subsetD] |
106 apply (blast intro: sym l_one subgroup.subset [THEN subsetD] |
107 subgroup.one_closed) |
107 subgroup.one_closed) |
108 done |
108 done |
109 |
109 |
110 text {* Opposite of @{thm [locale=group,source] "repr_independence"} *} |
110 text (in group) {* Opposite of @{thm [source] "repr_independence"} *} |
111 lemma (in group) repr_independenceD: |
111 lemma (in group) repr_independenceD: |
112 includes subgroup H G |
112 includes subgroup H G |
113 assumes ycarr: "y \<in> carrier G" |
113 assumes ycarr: "y \<in> carrier G" |
114 and repr: "H #> x = H #> y" |
114 and repr: "H #> x = H #> y" |
115 shows "y \<in> H #> x" |
115 shows "y \<in> H #> x" |
116 by (subst repr, intro rcos_self) |
116 apply (subst repr) |
|
117 apply (intro rcos_self) |
|
118 apply (rule ycarr) |
|
119 apply (rule is_subgroup) |
|
120 done |
117 |
121 |
118 text {* Elements of a right coset are in the carrier *} |
122 text {* Elements of a right coset are in the carrier *} |
119 lemma (in subgroup) elemrcos_carrier: |
123 lemma (in subgroup) elemrcos_carrier: |
120 includes group |
124 includes group |
121 assumes acarr: "a \<in> carrier G" |
125 assumes acarr: "a \<in> carrier G" |
817 |
821 |
818 lemma (in subgroup) subgroup_in_rcosets: |
822 lemma (in subgroup) subgroup_in_rcosets: |
819 includes group G |
823 includes group G |
820 shows "H \<in> rcosets H" |
824 shows "H \<in> rcosets H" |
821 proof - |
825 proof - |
822 have "H #> \<one> = H" |
826 from _ `subgroup H G` have "H #> \<one> = H" |
823 by (rule coset_join2, auto) |
827 by (rule coset_join2) auto |
824 then show ?thesis |
828 then show ?thesis |
825 by (auto simp add: RCOSETS_def) |
829 by (auto simp add: RCOSETS_def) |
826 qed |
830 qed |
827 |
831 |
828 lemma (in normal) rcosets_inv_mult_group_eq: |
832 lemma (in normal) rcosets_inv_mult_group_eq: |