isabelle: src/HOL/GroupTheory/Exponent.thy@05631e8f0258 (annotated)

11370 680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	1	(* Title: HOL/GroupTheory/Exponent
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	2	ID: $Id$
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	3	Author: Florian Kammueller, with new proofs by L C Paulson
11394 e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	4	Copyright 1998-2001 University of Cambridge
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	5
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	6	The combinatorial argument underlying the first Sylow theorem
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	7
e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	8	exponent p s yields the greatest power of p that divides s.
11370 680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	9	*)
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	10
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	11	Exponent = Main + Primes +
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	12
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	13	constdefs
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	14
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	15	exponent :: "[nat, nat] => nat"
11394 e88c2c89f98e Locale-based group theory proofs paulson parents: 11370 diff changeset	16	"exponent p s == if p \\<in> prime then (GREATEST r. p^r dvd s) else 0"
11370 680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	17
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version) paulson parents: diff changeset	18	end

author	paulson
	Wed, 31 Jul 2002 14:34:08 +0200
changeset 13435	05631e8f0258
parent 11394	e88c2c89f98e
child 13583	5fcc8bf538ee
permissions	-rw-r--r--