isabelle: src/HOL/Algebra/README.html@3d0c34795831 (annotated)

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	<!-- $Id$ -->
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	<H2>Algebra: Theories of Rings and Polynomials</H2>
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	<P>This development of univariate polynomials is separated into an
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	7	abstract development of rings and the development of polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	8	itself. The formalisation is based on [Jacobson1985], and polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	9	have a sparse, mathematical representation. These theories were
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	10	developed as a base for the integration of a computer algebra system
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11	to Isabelle [Ballarin1999], and was designed to match implementations
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	12	of these domains in some typed computer algebra systems. Summary:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	13
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	14	<P><EM>Rings:</EM>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15	Classes of rings are represented by axiomatic type classes. The
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	16	following are available:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	17
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	18	<PRE>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	19	ringS: Syntactic class
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	20	ring: Commutative rings with one (including a summation
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	21	operator, which is needed for the polynomials)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	22	domain: Integral domains
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	23	factorial: Factorial domains (divisor chain condition is missing)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	24	pid: Principal ideal domains
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	25	field: Fields
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	26	</PRE>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	27
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	28	Also, some facts about ring homomorphisms and ideals are mechanised.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	29
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	30	<P><EM>Polynomials:</EM>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	31	Polynomials have a natural, mathematical representation. Facts about
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	32	the following topics are provided:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	33
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	34	<MENU>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	35	<LI>Degree function
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	36	<LI> Universal Property, evaluation homomorphism
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	37	<LI>Long division (existence and uniqueness)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	38	<LI>Polynomials over a ring form a ring
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	39	<LI>Polynomials over an integral domain form an integral domain
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	40	</MENU>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	41
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	42	<P>Still missing are
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	43	Polynomials over a factorial domain form a factorial domain
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	44	(difficult), and polynomials over a field form a pid.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	45
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	46	<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	47
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	48	<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	49	Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	50
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	51	<HR>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	52	<P>Last modified on $Date$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	53
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	54	<ADDRESS>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	55	<P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>. Karlsruhe, October 1999
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	56
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	57	<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	58	</ADDRESS>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	59	</BODY></HTML>

author	paulson
	Fri, 05 Nov 1999 11:14:26 +0100
changeset 7998	3d0c34795831
child 13944	9b34607cd83e
permissions	-rw-r--r--