equal
deleted
inserted
replaced
10 |
10 |
11 section {*Sylow's Theorem*} |
11 section {*Sylow's Theorem*} |
12 |
12 |
13 subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} |
13 subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} |
14 |
14 |
15 definition exponent :: "nat => nat => nat" where |
15 definition |
16 "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" |
16 exponent :: "nat => nat => nat" |
|
17 where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)" |
17 |
18 |
18 |
19 |
19 text{*Prime Theorems*} |
20 text{*Prime Theorems*} |
20 |
21 |
21 lemma prime_imp_one_less: "prime p ==> Suc 0 < p" |
22 lemma prime_imp_one_less: "prime p ==> Suc 0 < p" |