isabelle: src/HOL/Algebra/abstract/Field.thy@df149b8c86b8 (annotated)

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	(*
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	Properties of abstract class field
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3	$Id$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	Author: Clemens Ballarin, started 15 November 1997
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	6
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	7	theory Field imports Factor PID begin
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	8
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	9	instance field < "domain"
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	10	apply intro_classes
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	11	apply (rule field_one_not_zero)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	12	apply (erule field_integral)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	13	done
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	15	instance field < factorial
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	16	apply intro_classes
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	17	apply (rule TrueI)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	18	apply (erule field_fact_prime)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	19	done
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	20
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	21	end

author	wenzelm
	Tue, 07 Nov 2006 19:39:53 +0100
changeset 21231	df149b8c86b8
parent 17479	68a7acb5f22e
child 29665	2b956243d123
permissions	-rw-r--r--