Abstract: 
This entry formalizes 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 fieldtheoretic Nullstellensatz. The formalization follows
Chapter 4.1. of Ideals,
Varieties, and Algorithms by Cox, Little and O'Shea. 
BibTeX: 
@article{NullstellensatzAFP,
author = {Alexander Maletzky},
title = {Hilbert's Nullstellensatz},
journal = {Archive of Formal Proofs},
month = jun,
year = 2019,
note = {\url{https://isaafp.org/entries/Nullstellensatz.html},
Formal proof development},
ISSN = {2150914x},
}
