isabelle: src/HOL/Algebra/abstract/Field.thy@98809b3f5e3c (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	Author: Clemens Ballarin, started 15 November 1997
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
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	6	theory Field imports Factor PID begin
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	7
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	8	instance field < "domain"
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	9	apply intro_classes
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	10	apply (rule field_one_not_zero)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	11	apply (erule field_integral)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	12	done
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	14	instance field < factorial
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	15	apply intro_classes
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	16	apply (erule field_fact_prime)
68a7acb5f22e converted to Isar theory format; wenzelm parents: 11093 diff changeset	17	done
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	18
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	19	end

author	nipkow
	Wed, 01 Apr 2009 18:41:15 +0200
changeset 30840	98809b3f5e3c
parent 29665	2b956243d123
child 35849	b5522b51cb1e
permissions	-rw-r--r--