Email Gateway (Aug 22 2022 at 13:21): Email Gateway (Aug 22 2022 at 13:21):From: Tobias Nipkow <nipkow@in.tum.de>
Gröbner Bases Theory
Fabian Immler, Alexander Maletzky
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.
http://www.isa-afp.org/entries/Groebner_Bases.shtml
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC