src/HOL/Algebra/Exponent.thy
changeset 27717 21bbd410ba04
parent 27651 16a26996c30e
child 30011 cc264a9a033d
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Fri Aug 01 17:41:37 2008 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Fri Aug 01 18:10:52 2008 +0200
     1.3 @@ -9,12 +9,15 @@
     1.4  imports Main Primes Binomial
     1.5  begin
     1.6  
     1.7 -section {*The Combinatorial Argument Underlying the First Sylow Theorem*}
     1.8 +section {*Sylow's Theorem*}
     1.9 +
    1.10 +subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}
    1.11 +
    1.12  definition exponent :: "nat => nat => nat" where
    1.13  "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
    1.14  
    1.15  
    1.16 -subsection{*Prime Theorems*}
    1.17 +text{*Prime Theorems*}
    1.18  
    1.19  lemma prime_imp_one_less: "prime p ==> Suc 0 < p"
    1.20  by (unfold prime_def, force)
    1.21 @@ -106,7 +109,7 @@
    1.22  done
    1.23  
    1.24  
    1.25 -subsection{*Exponent Theorems*}
    1.26 +text{*Exponent Theorems*}
    1.27  
    1.28  lemma exponent_ge [rule_format]:
    1.29    "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
    1.30 @@ -186,7 +189,7 @@
    1.31  done
    1.32  
    1.33  
    1.34 -subsection{*Main Combinatorial Argument*}
    1.35 +text{*Main Combinatorial Argument*}
    1.36  
    1.37  lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
    1.38  apply (rule_tac P = "%x. x <= b * c" in subst)