Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Hilbert Basis Theorem?

Email Gateway (Feb 14 2023 at 17:55):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hello,

is there Hibert Basis Therem in some form in Isabelle?
I mean the theorem that any polynomial ideal over a Noetherian ring
(say, int) is finitely generated.

Best regards

Stepan

Email Gateway (Feb 15 2023 at 10:52):

From: Wenda Li <wl302@cam.ac.uk>
Hi Stepan,

I don’t know if we have Hibert Basis Therem yet, but there are related ones like Hilbert's Nullstellensatz and Gröbner bases in the AFP:

<https://www.isa-afp.org/entries/Nullstellensatz.html>
[afp.png]
Hilbert's Nullstellensatz<https://www.isa-afp.org/entries/Nullstellensatz.html>
isa-afp.org<https://www.isa-afp.org/entries/Nullstellensatz.html>

<https://www.isa-afp.org/entries/Groebner_Bases.html>
[afp.png]
Gröbner Bases Theory<https://www.isa-afp.org/entries/Groebner_Bases.html>
isa-afp.org<https://www.isa-afp.org/entries/Groebner_Bases.html>

Regards,
Wenda

afp.png
afp.png

Last updated: Jan 04 2025 at 20:18 UTC