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