author | eberlm |
Fri, 17 Jun 2016 11:33:52 +0200 | |
changeset 63319 | bc8793d7bd21 |
parent 62410 | 2fc7a8d9c529 |
child 63534 | 523b488b15c9 |
permissions | -rw-r--r-- |
14706 | 1 |
(* Title: HOL/Algebra/Exponent.thy |
35849 | 2 |
Author: Florian Kammueller |
3 |
Author: L C Paulson |
|
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
4 |
|
35849 | 5 |
exponent p s yields the greatest power of p that divides s. |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
6 |
*) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
7 |
|
27105
5f139027c365
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
25162
diff
changeset
|
8 |
theory Exponent |
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
58917
diff
changeset
|
9 |
imports Main "~~/src/HOL/Number_Theory/Primes" |
27105
5f139027c365
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
25162
diff
changeset
|
10 |
begin |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset
|
11 |
|
61382 | 12 |
section \<open>Sylow's Theorem\<close> |
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27651
diff
changeset
|
13 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
14 |
text \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close> |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
15 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
16 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
17 |
subsection\<open>Prime Theorems\<close> |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
18 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
19 |
lemma prime_dvd_cases: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
20 |
assumes pk: "p*k dvd m*n" and p: "prime p" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
21 |
shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
22 |
proof - |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
23 |
have "p dvd m*n" using dvd_mult_left pk by blast |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
24 |
then consider "p dvd m" | "p dvd n" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
25 |
using p prime_dvd_mult_eq_nat by blast |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
26 |
then show ?thesis |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
27 |
proof cases |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
28 |
case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
29 |
then have "\<exists>x. k dvd x * n \<and> m = p * x" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
30 |
using p pk by auto |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
31 |
then show ?thesis .. |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
32 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
33 |
case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
34 |
then have "\<exists>y. k dvd m*y \<and> n = p*y" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
35 |
using p pk by auto |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
36 |
then show ?thesis .. |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
37 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
38 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
39 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
40 |
lemma prime_power_dvd_prod: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
41 |
assumes pc: "p^c dvd m*n" and p: "prime p" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
42 |
shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
43 |
using pc |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
44 |
proof (induct c arbitrary: m n) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
45 |
case 0 show ?case by simp |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
46 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
47 |
case (Suc c) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
48 |
consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
49 |
using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
50 |
then show ?case |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
51 |
proof cases |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
52 |
case (1 x) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
53 |
with Suc.hyps [of x n] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
54 |
by force |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
55 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
56 |
case (2 y) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
57 |
with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
58 |
by force |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
59 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
60 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
61 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
62 |
lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
63 |
by arith |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
64 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
65 |
lemma prime_power_dvd_cases: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
66 |
"\<lbrakk>p^c dvd m * n; a + b = Suc c; prime p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
67 |
using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
68 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
69 |
text\<open>needed in this form to prove Sylow's theorem\<close> |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
70 |
corollary div_combine: "\<lbrakk>prime p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
71 |
by (metis add_Suc_right mult.commute prime_power_dvd_cases) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
72 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
73 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
74 |
subsection\<open>The Exponent Function\<close> |
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27651
diff
changeset
|
75 |
|
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
32946
diff
changeset
|
76 |
definition |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
32946
diff
changeset
|
77 |
exponent :: "nat => nat => nat" |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
32946
diff
changeset
|
78 |
where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)" |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
79 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
80 |
lemma exponent_eq_0 [simp]: "\<not> prime p \<Longrightarrow> exponent p s = 0" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
81 |
by (simp add: exponent_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset
|
82 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
83 |
lemma Suc_le_power: "Suc 0 < p \<Longrightarrow> Suc n \<le> p ^ n" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
84 |
by (induct n) (auto simp: Suc_le_eq le_less_trans) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
85 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
86 |
text\<open>An upper bound for the @{term n} such that @{term"p^n dvd a"}: needed for GREATEST to exist\<close> |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
87 |
lemma power_dvd_bound: "\<lbrakk>p ^ n dvd a; Suc 0 < p; 0 < a\<rbrakk> \<Longrightarrow> n < a" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
88 |
by (meson Suc_le_lessD Suc_le_power dvd_imp_le le_trans) |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
89 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
90 |
lemma exponent_ge: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
91 |
assumes "p ^ k dvd n" "prime p" "0 < n" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
92 |
shows "k \<le> exponent p n" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
93 |
proof - |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
94 |
have "Suc 0 < p" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
95 |
using \<open>prime p\<close> by (simp add: prime_def) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
96 |
with assms show ?thesis |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
97 |
by (simp add: \<open>prime p\<close> exponent_def) (meson Greatest_le power_dvd_bound) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
98 |
qed |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
99 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
100 |
lemma power_exponent_dvd: "p ^ exponent p s dvd s" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
101 |
proof (cases "s = 0") |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
102 |
case True then show ?thesis by simp |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
103 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
104 |
case False then show ?thesis |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
105 |
apply (simp add: exponent_def, clarify) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
106 |
apply (rule GreatestI [where k = 0]) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
107 |
apply (auto dest: prime_gt_Suc_0_nat power_dvd_bound) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
108 |
done |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
109 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
110 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
111 |
lemma power_Suc_exponent_Not_dvd: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
112 |
"\<lbrakk>p * p ^ exponent p s dvd s; prime p\<rbrakk> \<Longrightarrow> s = 0" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
113 |
by (metis exponent_ge neq0_conv not_less_eq_eq order_refl power_Suc) |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
114 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
115 |
lemma exponent_power_eq [simp]: "prime p \<Longrightarrow> exponent p (p ^ a) = a" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
116 |
apply (simp add: exponent_def) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
117 |
apply (rule Greatest_equality, simp) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
118 |
apply (simp add: prime_gt_Suc_0_nat power_dvd_imp_le) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
119 |
done |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
120 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
121 |
lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
122 |
apply (case_tac "prime p") |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
123 |
apply (metis exponent_power_eq nat_power_eq_Suc_0_iff) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
124 |
apply simp |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
125 |
done |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
126 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
127 |
lemma exponent_equalityI: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
128 |
"(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> exponent p a = exponent p b" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
129 |
by (simp add: exponent_def) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
130 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
131 |
lemma exponent_mult_add: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
132 |
assumes "a > 0" "b > 0" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
133 |
shows "exponent p (a * b) = (exponent p a) + (exponent p b)" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
134 |
proof (cases "prime p") |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
135 |
case False then show ?thesis by simp |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
136 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
137 |
case True show ?thesis |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
138 |
proof (rule order_antisym) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
139 |
show "exponent p a + exponent p b \<le> exponent p (a * b)" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
140 |
by (rule exponent_ge) (auto simp: mult_dvd_mono power_add power_exponent_dvd \<open>prime p\<close> assms) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
141 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
142 |
{ assume "exponent p a + exponent p b < exponent p (a * b)" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
143 |
then have "p ^ (Suc (exponent p a + exponent p b)) dvd a * b" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
144 |
by (meson Suc_le_eq power_exponent_dvd power_le_dvd) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
145 |
with prime_power_dvd_cases [where a = "Suc (exponent p a)" and b = "Suc (exponent p b)"] |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
146 |
have False |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
147 |
by (metis Suc_n_not_le_n True add_Suc add_Suc_right assms exponent_ge) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
148 |
} |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
149 |
then show "exponent p (a * b) \<le> exponent p a + exponent p b" by (blast intro: leI) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
150 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
151 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
152 |
|
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
153 |
lemma not_divides_exponent_0: "~ (p dvd n) \<Longrightarrow> exponent p n = 0" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
154 |
apply (case_tac "exponent p n", simp) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
155 |
by (metis dvd_mult_left power_Suc power_exponent_dvd) |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
156 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
157 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
158 |
subsection\<open>The Main Combinatorial Argument\<close> |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
159 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
160 |
lemma exponent_p_a_m_k_equation: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
161 |
assumes "0 < m" "0 < k" "p \<noteq> 0" "k < p^a" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
162 |
shows "exponent p (p^a * m - k) = exponent p (p^a - k)" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
163 |
proof (rule exponent_equalityI [OF iffI]) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
164 |
fix r |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
165 |
assume *: "p ^ r dvd p ^ a * m - k" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
166 |
show "p ^ r dvd p ^ a - k" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
167 |
proof - |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
168 |
have "k \<le> p ^ a * m" using assms |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
169 |
by (meson nat_dvd_not_less dvd_triv_left leI mult_pos_pos order.strict_trans) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
170 |
then have "r \<le> a" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
171 |
by (meson "*" \<open>0 < k\<close> \<open>k < p^a\<close> dvd_diffD1 dvd_triv_left leI less_imp_le_nat nat_dvd_not_less power_le_dvd) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
172 |
then have "p^r dvd p^a * m" by (simp add: le_imp_power_dvd) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
173 |
thus ?thesis |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
174 |
by (meson \<open>k \<le> p ^ a * m\<close> \<open>r \<le> a\<close> * dvd_diffD1 dvd_diff_nat le_imp_power_dvd) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
175 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
176 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
177 |
fix r |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
178 |
assume *: "p ^ r dvd p ^ a - k" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
179 |
with assms have "r \<le> a" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
180 |
by (metis diff_diff_cancel less_imp_le_nat nat_dvd_not_less nat_le_linear power_le_dvd zero_less_diff) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
181 |
show "p ^ r dvd p ^ a * m - k" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
182 |
proof - |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
183 |
have "p^r dvd p^a*m" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
184 |
by (simp add: \<open>r \<le> a\<close> le_imp_power_dvd) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
185 |
then show ?thesis |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
186 |
by (meson assms * dvd_diffD1 dvd_diff_nat le_imp_power_dvd less_imp_le_nat \<open>r \<le> a\<close>) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
187 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
188 |
qed |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
189 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
190 |
lemma p_not_div_choose_lemma: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
191 |
assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> exponent p (Suc i) = exponent p (Suc (j + i))" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
192 |
and "k < K" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
193 |
shows "exponent p (j + k choose k) = 0" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
194 |
proof (cases "prime p") |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
195 |
case False then show ?thesis by simp |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
196 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
197 |
case True show ?thesis using \<open>k < K\<close> |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
198 |
proof (induction k) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
199 |
case 0 then show ?case by simp |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
200 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
201 |
case (Suc k) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
202 |
then have *: "(Suc (j+k) choose Suc k) > 0" by simp |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
203 |
then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
204 |
by (metis Suc.IH Suc.prems Suc_lessD Suc_times_binomial_eq add.comm_neutral eeq exponent_mult_add |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
205 |
mult_pos_pos zero_less_Suc zero_less_mult_pos) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
206 |
then show ?case |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
207 |
by (metis * add.commute add_Suc_right add_eq_self_zero exponent_mult_add zero_less_Suc) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
208 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
209 |
qed |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
210 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
211 |
text\<open>The lemma above, with two changes of variables\<close> |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
212 |
lemma p_not_div_choose: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
213 |
assumes "k < K" and "k \<le> n" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
214 |
and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> exponent p (n - k + (K - j)) = exponent p (K - j)" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
215 |
shows "exponent p (n choose k) = 0" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
216 |
apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1]) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
217 |
apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
218 |
apply (rule TrueI) |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
219 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
220 |
|
62410
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
221 |
proposition const_p_fac: |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
222 |
assumes "m>0" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
223 |
shows "exponent p (p^a * m choose p^a) = exponent p m" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
224 |
proof (cases "prime p") |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
225 |
case False then show ?thesis by auto |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
226 |
next |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
227 |
case True |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
228 |
with assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
229 |
by (auto simp: prime_gt_0_nat) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
230 |
have *: "exponent p ((p^a * m - 1) choose (p^a - 1)) = 0" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
231 |
apply (rule p_not_div_choose [where K = "p^a"]) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
232 |
using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
233 |
have "exponent p ((p ^ a * m choose p ^ a) * p ^ a) = a + exponent p m" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
234 |
proof - |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
235 |
have "p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1)) = p ^ a * (p ^ a * m choose p ^ a)" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
236 |
using p One_nat_def times_binomial_minus1_eq by presburger |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
237 |
moreover have "exponent p (p ^ a) = a" |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
238 |
by (meson True exponent_power_eq) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
239 |
ultimately show ?thesis |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
240 |
using * p |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
241 |
by (metis (no_types, lifting) One_nat_def exponent_1_eq_0 exponent_mult_add mult.commute mult.right_neutral nat_0_less_mult_iff zero_less_binomial) |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
242 |
qed |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
243 |
then show ?thesis |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
244 |
using True p exponent_mult_add by auto |
2fc7a8d9c529
partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents:
62349
diff
changeset
|
245 |
qed |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
246 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
247 |
end |