Prove2Me

I(V(J))=J\mathrm I(\mathrm V(J)) = \sqrt J

Proved
Nullstellensatz.vanishingIdeal_zeroSet_eq_radical

by Lucas · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrycommutative-algebra

Let KK be an algebraically closed field and JJ an ideal of K[X1,…,Xn]K[X_1,\dots,X_n]. Then

I(V(J))=J,\mathrm I(\mathrm V(J)) = \sqrt J,

where V(J)⊆Kn\mathrm V(J) \subseteq K^n is the zero locus of JJ, I(U)\mathrm I(U) is the ideal of polynomials vanishing on UU, and J={p:pr∈J for some r∈N}\sqrt J = \{p : p^r \in J \text{ for some } r \in \mathbb N\} is the radical of JJ.

This is the formulation of the Nullstellensatz in the notation of algebraic geometry. The inclusion J⊆I(V(J))\sqrt J \subseteq \mathrm I(\mathrm V(J)) follows from the definitions.

Preamble
import Definitions.Def_Nullstellensatz_Defs
import Mathlib

open MvPolynomial
Formal statement
namespace Nullstellensatz

theorem vanishingIdeal_zeroSet_eq_radical {K : Type*} [Field K] [IsAlgClosed K] {n : ℕ}
    (J : Ideal (MvPolynomial (Fin n) K)) :
    vanishingIdeal (zeroSet J) = J.radical := by sorry

end Nullstellensatz
Source
Wikipedia, article "Hilbert's Nullstellensatz" (snapshot supplied as Hilbert's_Nullstellensatz.pdf, printed 2026-09-27), https://en.wikipedia.org/wiki/Hilbert%27s_Nullstellensatz, section "Formulations", paragraph 2 (display I(V(J)) = sqrt J).
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source article and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence that the statement is faithful.

Let KK be an algebraically closed field, nn a natural number, and JJ any ideal of K[X1,…,Xn]K[X_1,\dots,X_n]. The statement is the equality of ideals

I(V(J))=J,\mathrm I(\mathrm V(J)) = \sqrt J,

where V(J)={a∈Kn:f(a)=0 ∀f∈J}\mathrm V(J) = \{a \in K^n : f(a) = 0 \ \forall f \in J\}, I(U)={p:p(a)=0 ∀a∈U}\mathrm I(U) = \{p : p(a) = 0 \ \forall a \in U\}, and J={p:∃r∈N, pr∈J}\sqrt J = \{p : \exists r \in \mathbb N,\ p^r \in J\} (Mathlib's radical). For JJ the whole ring both sides are the whole ring.

Human review

  • Endorsed by Shuze Chen · Sep 28, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Sep 28, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph