equal
deleted
inserted
replaced
411 by (rule group.rcos_disjoint [OF a_group a_subgroup, |
411 by (rule group.rcos_disjoint [OF a_group a_subgroup, |
412 folded A_RCOSETS_def, simplified monoid_record_simps]) |
412 folded A_RCOSETS_def, simplified monoid_record_simps]) |
413 |
413 |
414 lemma (in abelian_subgroup) a_rcos_self: |
414 lemma (in abelian_subgroup) a_rcos_self: |
415 shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x" |
415 shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x" |
416 by (rule group.rcos_self [OF a_group a_subgroup, |
416 by (rule group.rcos_self [OF a_group _ a_subgroup, |
417 folded a_r_coset_def, simplified monoid_record_simps]) |
417 folded a_r_coset_def, simplified monoid_record_simps]) |
418 |
418 |
419 lemma (in abelian_subgroup) a_rcosets_part_G: |
419 lemma (in abelian_subgroup) a_rcosets_part_G: |
420 shows "\<Union>(a_rcosets H) = carrier G" |
420 shows "\<Union>(a_rcosets H) = carrier G" |
421 by (rule group.rcosets_part_G [OF a_group a_subgroup, |
421 by (rule group.rcosets_part_G [OF a_group a_subgroup, |