Email Gateway (Aug 22 2022 at 20:01): Email Gateway (Aug 22 2022 at 20:01):From: Lawrence Paulson <lp15@cam.ac.uk>
Following on from this morning’s announcement of an entry on Gröbner Bases, I’m happy to announce a subsequent entry by the same author, on Hilbert's Nullstellensatz:
an important theorem in algebraic geometry that can be viewed as the generalization of the Fundamental Theorem of Algebra to multivariate polynomials: If a set of (multivariate) polynomials over an algebraically closed field has no common zero, then the ideal it generates is the entire polynomial ring. The formalization proves several equivalent versions of this celebrated theorem: the weak Nullstellensatz, the strong Nullstellensatz (connecting algebraic varieties and radical ideals), and the field-theoretic Nullstellensatz. The formalization follows Chapter 4.1. of Ideals, Varieties, and Algorithms by Cox, Little and O’Shea.
Many thanks to Alexander Maletzky for this additional entry! It is online at https://www.isa-afp.org/entries/Nullstellensatz.html
Larry Paulson
Last updated: Apr 25 2024 at 20:15 UTC