This file establishes a version of Hilbert's classical Nullstellensatz for
The main statement of the theorem is
The statement is in terms of new definitions
Mathlib already has versions of these in terms of the prime spectrum of a ring,
but those are not well-suited for expressing this result.
Suggestions for better ways to state this theorem or organize things are welcome.
The machinery around
zero_locus is also minimal, I only added lemmas
directly needed in this proof, since I'm not sure if they are the right approach.
Ideal of polynomials with common zeroes at all elements of a set