src/ZF/ex/Group.thy
changeset 58860 fee7cfa69c50
parent 49755 b286e8f47560
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/ex/Group.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/ZF/ex/Group.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -383,7 +383,7 @@
     1.4  apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)")
     1.5   prefer 2 apply (simp add: bij_converse_bij bij_is_fun)
     1.6  apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"]
     1.7 -            simp add: hom_def bij_is_inj right_inverse_bij);
     1.8 +            simp add: hom_def bij_is_inj right_inverse_bij)
     1.9  done
    1.10  
    1.11  lemma (in group) iso_trans:
    1.12 @@ -658,7 +658,7 @@
    1.13    by (simp add: normal_def subgroup_def)
    1.14  
    1.15  lemma (in group) normalI:
    1.16 -  "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
    1.17 +  "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
    1.18    by (simp add: normal_def normal_axioms_def)
    1.19  
    1.20  lemma (in normal) inv_op_closed1:
    1.21 @@ -1086,7 +1086,7 @@
    1.22  definition
    1.23    kernel :: "[i,i,i] => i" where
    1.24      --{*the kernel of a homomorphism*}
    1.25 -  "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}";
    1.26 +  "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}"
    1.27  
    1.28  lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
    1.29  apply (rule subgroup.intro)