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

35849 b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	1	(* Author: Clemens Ballarin, started 15 November 1997
b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	2
b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	3	Properties of abstract class field.
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5
35849 b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	6	theory Field
b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	7	imports Factor PID
b5522b51cb1e standard headers; wenzelm parents: 29665 diff changeset	8	begin
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	9
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	10	instance field < "domain"
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	11	apply intro_classes
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	12	apply (rule field_one_not_zero)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	13	apply (erule field_integral)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	14	done
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	16	instance field < factorial
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	17	apply intro_classes
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	blanchet
	Wed, 12 Sep 2012 17:26:05 +0200
changeset 49335	096967bf3940
parent 35849	b5522b51cb1e
permissions	-rw-r--r--