isabelle: src/HOL/GroupTheory/Exponent.thy@6766aa05e4eb (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	wenzelm
	Thu, 06 Dec 2001 00:39:40 +0100
changeset 12397	6766aa05e4eb
parent 11394	e88c2c89f98e
child 13583	5fcc8bf538ee
permissions	-rw-r--r--