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])
```