src/HOL/Algebra/AbelCoset.thy
changeset 67091 1393c2340eec
parent 63167 0909deb8059b
child 67443 3abf6a722518
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -290,7 +290,7 @@
     1.4  text\<open>Alternative characterization of normal subgroups\<close>
     1.5  lemma (in abelian_group) a_normal_inv_iff:
     1.6       "(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) = 
     1.7 -      (subgroup N \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
     1.8 +      (subgroup N \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<and> (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
     1.9        (is "_ = ?rhs")
    1.10  by (rule group.normal_inv_iff [OF a_group,
    1.11      folded a_inv_def, simplified monoid_record_simps])