equal
deleted
inserted
replaced
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 header{*The Combinatorial Argument Underlying the First Sylow Theorem*} |
8 header{*The Combinatorial Argument Underlying the First Sylow Theorem*} |
9 |
9 |
10 theory Exponent = Main + Primes: |
10 theory Exponent imports Main Primes begin |
11 |
11 |
12 constdefs |
12 constdefs |
13 exponent :: "[nat, nat] => nat" |
13 exponent :: "[nat, nat] => nat" |
14 "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0" |
14 "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0" |
15 |
15 |