equal
deleted
inserted
replaced
1377 thus "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \<in> H1K" using xhx_egal by simp |
1377 thus "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \<in> H1K" using xhx_egal by simp |
1378 qed |
1378 qed |
1379 qed |
1379 qed |
1380 qed |
1380 qed |
1381 |
1381 |
1382 lemma (in group) normal_inter_subgroup: |
1382 lemma (in group) normal_Int_subgroup: |
1383 assumes "subgroup H G" |
1383 assumes "subgroup H G" |
1384 and "N \<lhd> G" |
1384 and "N \<lhd> G" |
1385 shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)" |
1385 shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)" |
1386 proof - |
1386 proof - |
1387 define K where "K = carrier G" |
1387 define K where "K = carrier G" |