isabelle: src/HOL/Algebra/abstract/Field.thy@9fe28da848b0 (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
	Fri, 27 Jul 2007 16:31:15 +0200
changeset 24002	9fe28da848b0
parent 17479	68a7acb5f22e
child 29665	2b956243d123
permissions	-rw-r--r--