|
1 section \<open>Elementary Group Constructions\<close> |
|
2 |
|
3 (* Title: HOL/Algebra/Elementary_Groups.thy |
|
4 Author: LC Paulson, ported from HOL Light |
|
5 *) |
|
6 |
|
7 theory Elementary_Groups |
|
8 imports Generated_Groups |
|
9 begin |
|
10 |
|
11 subsection\<open>Direct sum/product lemmas\<close> |
|
12 |
|
13 locale group_disjoint_sum = group G + AG: subgroup A G + BG: subgroup B G for G (structure) and A B |
|
14 begin |
|
15 |
|
16 lemma subset_one: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> A \<inter> B = {\<one>}" |
|
17 by auto |
|
18 |
|
19 lemma sub_id_iff: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>)" |
|
20 (is "?lhs = ?rhs") |
|
21 proof - |
|
22 have "?lhs = (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> inv y = \<one> \<longrightarrow> x = \<one> \<and> inv y = \<one>)" |
|
23 proof (intro ballI iffI impI) |
|
24 fix x y |
|
25 assume "A \<inter> B \<subseteq> {\<one>}" "x \<in> A" "y \<in> B" "x \<otimes> inv y = \<one>" |
|
26 then have "y = x" |
|
27 using group.inv_equality group_l_invI by fastforce |
|
28 then show "x = \<one> \<and> inv y = \<one>" |
|
29 using \<open>A \<inter> B \<subseteq> {\<one>}\<close> \<open>x \<in> A\<close> \<open>y \<in> B\<close> by fastforce |
|
30 next |
|
31 assume "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> inv y = \<one> \<longrightarrow> x = \<one> \<and> inv y = \<one>" |
|
32 then show "A \<inter> B \<subseteq> {\<one>}" |
|
33 by auto |
|
34 qed |
|
35 also have "\<dots> = ?rhs" |
|
36 by (metis BG.mem_carrier BG.subgroup_axioms inv_inv subgroup_def) |
|
37 finally show ?thesis . |
|
38 qed |
|
39 |
|
40 lemma cancel: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y')" |
|
41 (is "?lhs = ?rhs") |
|
42 proof - |
|
43 have "(\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>) = ?rhs" |
|
44 (is "?med = _") |
|
45 proof (intro ballI iffI impI) |
|
46 fix x y x' y' |
|
47 assume * [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>" |
|
48 and AB: "x \<in> A" "y \<in> B" "x' \<in> A" "y' \<in> B" and eq: "x \<otimes> y = x' \<otimes> y'" |
|
49 then have carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" |
|
50 using AG.subset BG.subset by auto |
|
51 then have "inv x' \<otimes> x \<otimes> (y \<otimes> inv y') = inv x' \<otimes> (x \<otimes> y) \<otimes> inv y'" |
|
52 by (simp add: m_assoc) |
|
53 also have "\<dots> = \<one>" |
|
54 using carr by (simp add: eq) (simp add: m_assoc) |
|
55 finally have 1: "inv x' \<otimes> x \<otimes> (y \<otimes> inv y') = \<one>" . |
|
56 show "x = x' \<and> y = y'" |
|
57 using * [OF _ _ 1] AB by simp (metis carr inv_closed inv_inv local.inv_equality) |
|
58 next |
|
59 fix x y |
|
60 assume * [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y'" |
|
61 and xy: "x \<in> A" "y \<in> B" "x \<otimes> y = \<one>" |
|
62 show "x = \<one> \<and> y = \<one>" |
|
63 by (rule *) (use xy in auto) |
|
64 qed |
|
65 then show ?thesis |
|
66 by (simp add: sub_id_iff) |
|
67 qed |
|
68 |
|
69 lemma commuting_imp_normal1: |
|
70 assumes sub: "carrier G \<subseteq> A <#> B" |
|
71 and mult: "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x" |
|
72 shows "A \<lhd> G" |
|
73 proof - |
|
74 have AB: "A \<subseteq> carrier G \<and> B \<subseteq> carrier G" |
|
75 by (simp add: AG.subset BG.subset) |
|
76 have "A #> x = x <# A" |
|
77 if x: "x \<in> carrier G" for x |
|
78 proof - |
|
79 obtain a b where xeq: "x = a \<otimes> b" and "a \<in> A" "b \<in> B" and carr: "a \<in> carrier G" "b \<in> carrier G" |
|
80 using x sub AB by (force simp: set_mult_def) |
|
81 have Ab: "A <#> {b} = {b} <#> A" |
|
82 using AB \<open>a \<in> A\<close> \<open>b \<in> B\<close> mult |
|
83 by (force simp: set_mult_def m_assoc subset_iff) |
|
84 have "A #> x = A <#> {a \<otimes> b}" |
|
85 by (auto simp: l_coset_eq_set_mult r_coset_eq_set_mult xeq) |
|
86 also have "\<dots> = A <#> {a} <#> {b}" |
|
87 using AB \<open>a \<in> A\<close> \<open>b \<in> B\<close> |
|
88 by (auto simp: set_mult_def m_assoc subset_iff) |
|
89 also have "\<dots> = {a} <#> A <#> {b}" |
|
90 by (metis AG.rcos_const AG.subgroup_axioms \<open>a \<in> A\<close> coset_join3 is_group l_coset_eq_set_mult r_coset_eq_set_mult subgroup.mem_carrier) |
|
91 also have "\<dots> = {a} <#> {b} <#> A" |
|
92 by (simp add: is_group carr group.set_mult_assoc AB Ab) |
|
93 also have "\<dots> = {x} <#> A" |
|
94 by (auto simp: set_mult_def xeq) |
|
95 finally show "A #> x = x <# A" |
|
96 by (simp add: l_coset_eq_set_mult) |
|
97 qed |
|
98 then show ?thesis |
|
99 by (auto simp: normal_def normal_axioms_def AG.subgroup_axioms is_group) |
|
100 qed |
|
101 |
|
102 lemma commuting_imp_normal2: |
|
103 assumes"carrier G \<subseteq> A <#> B" "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x" |
|
104 shows "B \<lhd> G" |
|
105 proof (rule group_disjoint_sum.commuting_imp_normal1) |
|
106 show "group_disjoint_sum G B A" |
|
107 proof qed |
|
108 next |
|
109 show "carrier G \<subseteq> B <#> A" |
|
110 using BG.subgroup_axioms assms commut_normal commuting_imp_normal1 by blast |
|
111 qed (use assms in auto) |
|
112 |
|
113 |
|
114 lemma (in group) normal_imp_commuting: |
|
115 assumes "A \<lhd> G" "B \<lhd> G" "A \<inter> B \<subseteq> {\<one>}" "x \<in> A" "y \<in> B" |
|
116 shows "x \<otimes> y = y \<otimes> x" |
|
117 proof - |
|
118 interpret AG: normal A G |
|
119 using assms by auto |
|
120 interpret BG: normal B G |
|
121 using assms by auto |
|
122 interpret group_disjoint_sum G A B |
|
123 proof qed |
|
124 have * [rule_format]: "(\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y')" |
|
125 using cancel assms by (auto simp: normal_def) |
|
126 have carr: "x \<in> carrier G" "y \<in> carrier G" |
|
127 using assms AG.subset BG.subset by auto |
|
128 then show ?thesis |
|
129 using * [of x _ _ y] AG.coset_eq [rule_format, of y] BG.coset_eq [rule_format, of x] |
|
130 by (clarsimp simp: l_coset_def r_coset_def set_eq_iff) (metis \<open>x \<in> A\<close> \<open>y \<in> B\<close>) |
|
131 qed |
|
132 |
|
133 lemma normal_eq_commuting: |
|
134 assumes "carrier G \<subseteq> A <#> B" "A \<inter> B \<subseteq> {\<one>}" |
|
135 shows "A \<lhd> G \<and> B \<lhd> G \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)" |
|
136 by (metis assms commuting_imp_normal1 commuting_imp_normal2 normal_imp_commuting) |
|
137 |
|
138 lemma (in group) hom_group_mul_rev: |
|
139 assumes "(\<lambda>(x,y). x \<otimes> y) \<in> hom (subgroup_generated G A \<times>\<times> subgroup_generated G B) G" |
|
140 (is "?h \<in> hom ?P G") |
|
141 and "x \<in> carrier G" "y \<in> carrier G" "x \<in> A" "y \<in> B" |
|
142 shows "x \<otimes> y = y \<otimes> x" |
|
143 proof - |
|
144 interpret P: group_hom ?P G ?h |
|
145 by (simp add: assms DirProd_group group_hom.intro group_hom_axioms.intro is_group) |
|
146 have xy: "(x,y) \<in> carrier ?P" |
|
147 by (auto simp: assms carrier_subgroup_generated generate.incl) |
|
148 have "x \<otimes> (x \<otimes> (y \<otimes> y)) = x \<otimes> (y \<otimes> (x \<otimes> y))" |
|
149 using P.hom_mult [OF xy xy] by (simp add: m_assoc assms) |
|
150 then have "x \<otimes> (y \<otimes> y) = y \<otimes> (x \<otimes> y)" |
|
151 using assms by simp |
|
152 then show ?thesis |
|
153 by (simp add: assms flip: m_assoc) |
|
154 qed |
|
155 |
|
156 lemma hom_group_mul_eq: |
|
157 "(\<lambda>(x,y). x \<otimes> y) \<in> hom (subgroup_generated G A \<times>\<times> subgroup_generated G B) G |
|
158 \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)" |
|
159 (is "?lhs = ?rhs") |
|
160 proof |
|
161 assume ?lhs then show ?rhs |
|
162 using hom_group_mul_rev AG.subset BG.subset by blast |
|
163 next |
|
164 assume R: ?rhs |
|
165 have subG: "generate G (carrier G \<inter> A) \<subseteq> carrier G" for A |
|
166 by (simp add: generate_incl) |
|
167 have *: "x \<otimes> u \<otimes> (y \<otimes> v) = x \<otimes> y \<otimes> (u \<otimes> v)" |
|
168 if eq [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x" |
|
169 and gen: "x \<in> generate G (carrier G \<inter> A)" "y \<in> generate G (carrier G \<inter> B)" |
|
170 "u \<in> generate G (carrier G \<inter> A)" "v \<in> generate G (carrier G \<inter> B)" |
|
171 for x y u v |
|
172 proof - |
|
173 have "u \<otimes> y = y \<otimes> u" |
|
174 by (metis AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup carrier_subgroup_generated eq that(3) that(4)) |
|
175 then have "x \<otimes> u \<otimes> y = x \<otimes> y \<otimes> u" |
|
176 using gen by (simp add: m_assoc subsetD [OF subG]) |
|
177 then show ?thesis |
|
178 using gen by (simp add: subsetD [OF subG] flip: m_assoc) |
|
179 qed |
|
180 show ?lhs |
|
181 using R by (auto simp: hom_def carrier_subgroup_generated subsetD [OF subG] *) |
|
182 qed |
|
183 |
|
184 |
|
185 lemma epi_group_mul_eq: |
|
186 "(\<lambda>(x,y). x \<otimes> y) \<in> epi (subgroup_generated G A \<times>\<times> subgroup_generated G B) G |
|
187 \<longleftrightarrow> A <#> B = carrier G \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)" |
|
188 proof - |
|
189 have subGA: "generate G (carrier G \<inter> A) \<subseteq> A" |
|
190 by (simp add: AG.subgroup_axioms generate_subgroup_incl) |
|
191 have subGB: "generate G (carrier G \<inter> B) \<subseteq> B" |
|
192 by (simp add: BG.subgroup_axioms generate_subgroup_incl) |
|
193 have "(((\<lambda>(x, y). x \<otimes> y) ` (generate G (carrier G \<inter> A) \<times> generate G (carrier G \<inter> B)))) = ((A <#> B))" |
|
194 by (auto simp: set_mult_def generate.incl pair_imageI dest: subsetD [OF subGA] subsetD [OF subGB]) |
|
195 then show ?thesis |
|
196 by (auto simp: epi_def hom_group_mul_eq carrier_subgroup_generated) |
|
197 qed |
|
198 |
|
199 lemma mon_group_mul_eq: |
|
200 "(\<lambda>(x,y). x \<otimes> y) \<in> mon (subgroup_generated G A \<times>\<times> subgroup_generated G B) G |
|
201 \<longleftrightarrow> A \<inter> B = {\<one>} \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)" |
|
202 proof - |
|
203 have subGA: "generate G (carrier G \<inter> A) \<subseteq> A" |
|
204 by (simp add: AG.subgroup_axioms generate_subgroup_incl) |
|
205 have subGB: "generate G (carrier G \<inter> B) \<subseteq> B" |
|
206 by (simp add: BG.subgroup_axioms generate_subgroup_incl) |
|
207 show ?thesis |
|
208 apply (auto simp: mon_def hom_group_mul_eq simp flip: subset_one) |
|
209 apply (simp_all (no_asm_use) add: inj_on_def AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup) |
|
210 using cancel apply blast+ |
|
211 done |
|
212 qed |
|
213 |
|
214 lemma iso_group_mul_alt: |
|
215 "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G |
|
216 \<longleftrightarrow> A \<inter> B = {\<one>} \<and> A <#> B = carrier G \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)" |
|
217 by (auto simp: iso_iff_mon_epi mon_group_mul_eq epi_group_mul_eq) |
|
218 |
|
219 lemma iso_group_mul_eq: |
|
220 "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G |
|
221 \<longleftrightarrow> A \<inter> B = {\<one>} \<and> A <#> B = carrier G \<and> A \<lhd> G \<and> B \<lhd> G" |
|
222 by (simp add: iso_group_mul_alt normal_eq_commuting cong: conj_cong) |
|
223 |
|
224 |
|
225 lemma (in group) iso_group_mul_gen: |
|
226 assumes "A \<lhd> G" "B \<lhd> G" |
|
227 shows "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G |
|
228 \<longleftrightarrow> A \<inter> B \<subseteq> {\<one>} \<and> A <#> B = carrier G" |
|
229 proof - |
|
230 interpret group_disjoint_sum G A B |
|
231 using assms by (auto simp: group_disjoint_sum_def normal_def) |
|
232 show ?thesis |
|
233 by (simp add: subset_one iso_group_mul_eq assms) |
|
234 qed |
|
235 |
|
236 |
|
237 lemma iso_group_mul: |
|
238 assumes "comm_group G" |
|
239 shows "((\<lambda>(x,y). x \<otimes> y) \<in> iso (DirProd (subgroup_generated G A) (subgroup_generated G B)) G |
|
240 \<longleftrightarrow> A \<inter> B \<subseteq> {\<one>} \<and> A <#> B = carrier G)" |
|
241 proof (rule iso_group_mul_gen) |
|
242 interpret comm_group |
|
243 by (rule assms) |
|
244 show "A \<lhd> G" |
|
245 by (simp add: AG.subgroup_axioms subgroup_imp_normal) |
|
246 show "B \<lhd> G" |
|
247 by (simp add: BG.subgroup_axioms subgroup_imp_normal) |
|
248 qed |
|
249 |
|
250 end |
|
251 |
|
252 |
|
253 subsection\<open>The one-element group on a given object\<close> |
|
254 |
|
255 definition singleton_group :: "'a \<Rightarrow> 'a monoid" |
|
256 where "singleton_group a = \<lparr>carrier = {a}, monoid.mult = (\<lambda>x y. a), one = a\<rparr>" |
|
257 |
|
258 lemma singleton_group [simp]: "group (singleton_group a)" |
|
259 unfolding singleton_group_def by (auto intro: groupI) |
|
260 |
|
261 lemma singleton_abelian_group [simp]: "comm_group (singleton_group a)" |
|
262 by (metis group.group_comm_groupI monoid.simps(1) singleton_group singleton_group_def) |
|
263 |
|
264 lemma carrier_singleton_group [simp]: "carrier (singleton_group a) = {a}" |
|
265 by (auto simp: singleton_group_def) |
|
266 |
|
267 lemma (in group) hom_into_singleton_iff [simp]: |
|
268 "h \<in> hom G (singleton_group a) \<longleftrightarrow> h \<in> carrier G \<rightarrow> {a}" |
|
269 by (auto simp: hom_def singleton_group_def) |
|
270 |
|
271 declare group.hom_into_singleton_iff [simp] |
|
272 |
|
273 lemma (in group) id_hom_singleton: "id \<in> hom (singleton_group \<one>) G" |
|
274 by (simp add: hom_def singleton_group_def) |
|
275 |
|
276 subsection\<open>Similarly, trivial groups\<close> |
|
277 |
|
278 definition trivial_group :: "('a, 'b) monoid_scheme \<Rightarrow> bool" |
|
279 where "trivial_group G \<equiv> group G \<and> carrier G = {one G}" |
|
280 |
|
281 lemma trivial_imp_finite_group: |
|
282 "trivial_group G \<Longrightarrow> finite(carrier G)" |
|
283 by (simp add: trivial_group_def) |
|
284 |
|
285 lemma trivial_singleton_group [simp]: "trivial_group(singleton_group a)" |
|
286 by (metis monoid.simps(2) partial_object.simps(1) singleton_group singleton_group_def trivial_group_def) |
|
287 |
|
288 lemma (in group) trivial_group_subset: |
|
289 "trivial_group G \<longleftrightarrow> carrier G \<subseteq> {one G}" |
|
290 using is_group trivial_group_def by fastforce |
|
291 |
|
292 lemma (in group) trivial_group: "trivial_group G \<longleftrightarrow> (\<exists>a. carrier G = {a})" |
|
293 unfolding trivial_group_def using one_closed is_group by fastforce |
|
294 |
|
295 lemma (in group) trivial_group_alt: |
|
296 "trivial_group G \<longleftrightarrow> (\<exists>a. carrier G \<subseteq> {a})" |
|
297 by (auto simp: trivial_group) |
|
298 |
|
299 lemma (in group) trivial_group_subgroup_generated: |
|
300 assumes "S \<subseteq> {one G}" |
|
301 shows "trivial_group(subgroup_generated G S)" |
|
302 proof - |
|
303 have "carrier (subgroup_generated G S) \<subseteq> {\<one>}" |
|
304 using generate_empty generate_one subset_singletonD assms |
|
305 by (fastforce simp add: carrier_subgroup_generated) |
|
306 then show ?thesis |
|
307 by (simp add: group.trivial_group_subset) |
|
308 qed |
|
309 |
|
310 lemma (in group) trivial_group_subgroup_generated_eq: |
|
311 "trivial_group(subgroup_generated G s) \<longleftrightarrow> carrier G \<inter> s \<subseteq> {one G}" |
|
312 apply (rule iffI) |
|
313 apply (force simp: trivial_group_def carrier_subgroup_generated generate.incl) |
|
314 by (metis subgroup_generated_restrict trivial_group_subgroup_generated) |
|
315 |
|
316 lemma isomorphic_group_triviality1: |
|
317 assumes "G \<cong> H" "group H" "trivial_group G" |
|
318 shows "trivial_group H" |
|
319 using assms |
|
320 by (auto simp: trivial_group_def is_iso_def iso_def group.is_monoid Group.group_def bij_betw_def hom_one) |
|
321 |
|
322 lemma isomorphic_group_triviality: |
|
323 assumes "G \<cong> H" "group G" "group H" |
|
324 shows "trivial_group G \<longleftrightarrow> trivial_group H" |
|
325 by (meson assms group.iso_sym isomorphic_group_triviality1) |
|
326 |
|
327 lemma (in group_hom) kernel_from_trivial_group: |
|
328 "trivial_group G \<Longrightarrow> kernel G H h = carrier G" |
|
329 by (auto simp: trivial_group_def kernel_def) |
|
330 |
|
331 lemma (in group_hom) image_from_trivial_group: |
|
332 "trivial_group G \<Longrightarrow> h ` carrier G = {one H}" |
|
333 by (auto simp: trivial_group_def) |
|
334 |
|
335 lemma (in group_hom) kernel_to_trivial_group: |
|
336 "trivial_group H \<Longrightarrow> kernel G H h = carrier G" |
|
337 unfolding kernel_def trivial_group_def |
|
338 using hom_closed by blast |
|
339 |
|
340 |
|
341 subsection\<open>The additive group of integers\<close> |
|
342 |
|
343 definition integer_group |
|
344 where "integer_group = \<lparr>carrier = UNIV, monoid.mult = (+), one = (0::int)\<rparr>" |
|
345 |
|
346 lemma group_integer_group [simp]: "group integer_group" |
|
347 unfolding integer_group_def |
|
348 proof (rule groupI; simp) |
|
349 show "\<And>x::int. \<exists>y. y + x = 0" |
|
350 by presburger |
|
351 qed |
|
352 |
|
353 lemma carrier_integer_group [simp]: "carrier integer_group = UNIV" |
|
354 by (auto simp: integer_group_def) |
|
355 |
|
356 lemma one_integer_group [simp]: "\<one>\<^bsub>integer_group\<^esub> = 0" |
|
357 by (auto simp: integer_group_def) |
|
358 |
|
359 lemma mult_integer_group [simp]: "x \<otimes>\<^bsub>integer_group\<^esub> y = x + y" |
|
360 by (auto simp: integer_group_def) |
|
361 |
|
362 lemma inv_integer_group [simp]: "inv\<^bsub>integer_group\<^esub> x = -x" |
|
363 by (rule group.inv_equality [OF group_integer_group]) (auto simp: integer_group_def) |
|
364 |
|
365 lemma abelian_integer_group: "comm_group integer_group" |
|
366 by (rule group.group_comm_groupI [OF group_integer_group]) (auto simp: integer_group_def) |
|
367 |
|
368 lemma group_nat_pow_integer_group [simp]: |
|
369 fixes n::nat and x::int |
|
370 shows "pow integer_group x n = int n * x" |
|
371 by (induction n) (auto simp: integer_group_def algebra_simps) |
|
372 |
|
373 lemma group_int_pow_integer_group [simp]: |
|
374 fixes n::int and x::int |
|
375 shows "pow integer_group x n = n * x" |
|
376 by (simp add: int_pow_def2) |
|
377 |
|
378 lemma (in group) hom_integer_group_pow: |
|
379 "x \<in> carrier G \<Longrightarrow> pow G x \<in> hom integer_group G" |
|
380 by (rule homI) (auto simp: int_pow_mult) |
|
381 |
|
382 end |