Gröbner Bases Theory

Title:	Gröbner Bases Theory
Authors:	Fabian Immler and Alexander Maletzky
Submission date:	2016-05-02
Abstract:	This formalization is concerned with the theory of Gröbner bases in (commutative) multivariate polynomial rings over fields, originally developed by Buchberger in his 1965 PhD thesis. Apart from the statement and proof of the main theorem of the theory, the formalization also implements Buchberger's algorithm for actually computing Gröbner bases as a tail-recursive function, thus allowing to effectively decide ideal membership in finitely generated polynomial ideals. Furthermore, all functions can be executed on a concrete representation of multivariate polynomials as association lists.
Change history:	[2019-04-18]: Specialized Gröbner bases to less abstract representation of polynomials, where power-products are represented as polynomial mappings.
BibTeX:	@article{Groebner_Bases-AFP, author = {Fabian Immler and Alexander Maletzky}, title = {Gröbner Bases Theory}, journal = {Archive of Formal Proofs}, month = may, year = 2016, note = {\url{http://isa-afp.org/entries/Groebner_Bases.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Deriving, Jordan_Normal_Form, Polynomials
Used by:	Groebner_Macaulay, Nullstellensatz, Signature_Groebner
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.