equal
deleted
inserted
replaced
4 |
4 |
5 exponent p s yields the greatest power of p that divides s. |
5 exponent p s yields the greatest power of p that divides s. |
6 *) |
6 *) |
7 |
7 |
8 theory Exponent |
8 theory Exponent |
9 imports Main "~~/src/HOL/Old_Number_Theory/Primes" Binomial |
9 imports Main "~~/src/HOL/Old_Number_Theory/Primes" "~~/src/HOL/Library/Binomial" |
10 begin |
10 begin |
11 |
11 |
12 section {*Sylow's Theorem*} |
12 section {*Sylow's Theorem*} |
13 |
13 |
14 subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} |
14 subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} |