### 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 field-theoretic Nullstellensatz. The formalization follows Chapter 4.1. of Ideals, Varieties, and Algorithms by Cox, Little and O'Shea.

### License

BSD License

### Topics

- Mathematics/Algebra
- Mathematics/Geometry

### Session Nullstellensatz

- Algebraically_Closed_Fields
- Lex_Order_PP
- Univariate_PM
- Nullstellensatz
- Nullstellensatz_Field

### Depends on

- Gröbner Bases Theory

### Auto-related entries

- Perfect Fields
- Formal Puiseux Series
- The Transcendence of Certain Infinite Series
- Smooth Manifolds
- The Transcendence of π

## Cite

×

Nullstellensatz-AFP

    @article{Nullstellensatz-AFP,
      author  = {Alexander Maletzky},
      title   = {Hilbert's Nullstellensatz},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Nullstellensatz.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 17, 2019 : Isabelle2019