GitHub - amaletzk/Isabelle-Groebner: Isabelle/HOL formalization of advanced concepts of Groebner bases theory

This repository contains the Isabelle/HOL source files of the formalization of various advanced concepts in the theory of Groebner bases, including

a method for computing Groebner bases through Macaulay matrices,
degree-bounds of Groebner bases,
Hilbert's Nullstellensatz (both the geometric and the field-theoretic version), and
the Zariski topology.

The contents of this repository work with the development version of Isabelle. Sooner or later, all the theories are planned to be submitted to the Archive of Formal Proofs.

Name		Name	Last commit message	Last commit date
Latest commit History 340 Commits
Algebraically_Closed_Fields.thy		Algebraically_Closed_Fields.thy
Binom_Mult.thy		Binom_Mult.thy
Binomial_Int.thy		Binomial_Int.thy
Binomials.thy		Binomials.thy
Buchberger_Timings.thy		Buchberger_Timings.thy
Cone_Decomposition.thy		Cone_Decomposition.thy
Degree_Bound_Utils.thy		Degree_Bound_Utils.thy
Degree_Section.thy		Degree_Section.thy
Dube_Bound.thy		Dube_Bound.thy
Dube_Prelims.thy		Dube_Prelims.thy
Elimination_Property.thy		Elimination_Property.thy
Finite_Field.thy		Finite_Field.thy
Fun_Conv.thy		Fun_Conv.thy
GB_Bound_Binomials.thy		GB_Bound_Binomials.thy
General_Utils.thy		General_Utils.thy
Groebner_Macaulay.thy		Groebner_Macaulay.thy
Groebner_Macaulay_Examples.thy		Groebner_Macaulay_Examples.thy
Hilbert_Function.thy		Hilbert_Function.thy
Int31.thy		Int31.thy
LICENSE		LICENSE
Lex_Order_PP.thy		Lex_Order_PP.thy
Membership_Bound_Binomials.thy		Membership_Bound_Binomials.thy
Monomial_Module.thy		Monomial_Module.thy
More_MPoly_PM.thy		More_MPoly_PM.thy
Nullstellensatz.thy		Nullstellensatz.thy
Nullstellensatz_Field.thy		Nullstellensatz_Field.thy
Poly_Fun.thy		Poly_Fun.thy
Poly_Utils.thy		Poly_Utils.thy
Power_Products_PM.thy		Power_Products_PM.thy
Print.thy		Print.thy
README.md		README.md
Signature_Timings.thy		Signature_Timings.thy
Two_Polynomials.thy		Two_Polynomials.thy
Univariate_PM.thy		Univariate_PM.thy
VPC.thy		VPC.thy
Zariski_Topology.thy		Zariski_Topology.thy

License

amaletzk/Isabelle-Groebner

Folders and files

Latest commit

History

Repository files navigation

About

Resources

License

Stars

Watchers

Forks

Languages