equal
deleted
inserted
replaced
28 |
28 |
29 locale normal = subgroup + group + |
29 locale normal = subgroup + group + |
30 assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)" |
30 assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)" |
31 |
31 |
32 abbreviation |
32 abbreviation |
33 normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60) |
33 normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60) where |
34 "H \<lhd> G \<equiv> normal H G" |
34 "H \<lhd> G \<equiv> normal H G" |
35 |
35 |
36 |
36 |
37 subsection {*Basic Properties of Cosets*} |
37 subsection {*Basic Properties of Cosets*} |
38 |
38 |