equal
deleted
inserted
replaced
287 lemma (in sylow_central) inj_GmodH_M: |
287 lemma (in sylow_central) inj_GmodH_M: |
288 "\<exists>g \<in> rcosets G H\<rightarrow>M. inj_on g (rcosets G H)" |
288 "\<exists>g \<in> rcosets G H\<rightarrow>M. inj_on g (rcosets G H)" |
289 apply (rule bexI) |
289 apply (rule bexI) |
290 apply (rule_tac [2] setrcos_H_funcset_M) |
290 apply (rule_tac [2] setrcos_H_funcset_M) |
291 apply (rule inj_onI) |
291 apply (rule inj_onI) |
292 apply (rotate_tac -2, simp) |
292 apply (simp) |
293 apply (rule trans [OF _ H_elem_map_eq]) |
293 apply (rule trans [OF _ H_elem_map_eq]) |
294 prefer 2 apply assumption |
294 prefer 2 apply assumption |
295 apply (rule H_elem_map_eq [symmetric, THEN trans], assumption) |
295 apply (rule H_elem_map_eq [symmetric, THEN trans], assumption) |
296 apply (rule coset_sum_minus1) |
296 apply (rule coset_sum_minus1) |
297 apply (erule_tac [2] H_elem_map_carrier)+ |
297 apply (erule_tac [2] H_elem_map_carrier)+ |