equal
deleted
inserted
replaced
136 lemma (in subgroup) rcos_const: |
136 lemma (in subgroup) rcos_const: |
137 includes group |
137 includes group |
138 assumes hH: "h \<in> H" |
138 assumes hH: "h \<in> H" |
139 shows "H #> h = H" |
139 shows "H #> h = H" |
140 apply (unfold r_coset_def) |
140 apply (unfold r_coset_def) |
141 apply rule apply rule |
141 apply rule |
142 apply clarsimp |
142 apply rule |
143 apply (intro subgroup.m_closed) |
143 apply clarsimp |
144 apply assumption+ |
144 apply (intro subgroup.m_closed) |
|
145 apply (rule is_subgroup) |
|
146 apply assumption |
|
147 apply (rule hH) |
145 apply rule |
148 apply rule |
146 apply simp |
149 apply simp |
147 proof - |
150 proof - |
148 fix h' |
151 fix h' |
149 assume h'H: "h' \<in> H" |
152 assume h'H: "h' \<in> H" |