
Gröbner
Bases
Theory
Title: 
Gröbner Bases Theory 
Authors:

Fabian Immler and
Alexander Maletzky

Submission date: 
20160502 
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 tailrecursive 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: 
[20190418]: Specialized Gröbner bases to less abstract representation of polynomials, where
powerproducts are represented as polynomial mappings.

BibTeX: 
@article{Groebner_BasesAFP,
author = {Fabian Immler and Alexander Maletzky},
title = {Gröbner Bases Theory},
journal = {Archive of Formal Proofs},
month = may,
year = 2016,
note = {\url{https://isaafp.org/entries/Groebner_Bases.html},
Formal proof development},
ISSN = {2150914x},
}

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.

