| author | nipkow |
| Mon, 13 May 2002 15:27:28 +0200 | |
| changeset 13145 | 59bc43b51aa2 |
| parent 11394 | e88c2c89f98e |
| child 13583 | 5fcc8bf538ee |
| permissions | -rw-r--r-- |
(* Title: HOL/GroupTheory/Exponent ID: $Id$ Author: Florian Kammueller, with new proofs by L C Paulson Copyright 1998-2001 University of Cambridge The combinatorial argument underlying the first Sylow theorem exponent p s yields the greatest power of p that divides s. *) Exponent = Main + Primes + constdefs exponent :: "[nat, nat] => nat" "exponent p s == if p \\<in> prime then (GREATEST r. p^r dvd s) else 0" end