Prove2Me

I({a})=(X1−a1,…,Xn−an)\mathrm I(\{a\}) = (X_1 - a_1, \dots, X_n - a_n) is maximal

Proved
Nullstellensatz.vanishingIdeal_singleton

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

algebraic-geometrycommutative-algebra

Let KK be algebraically closed and a=(a1,…,an)∈Kna = (a_1,\dots,a_n) \in K^n. Then

I({a})=(X1−a1,…,Xn−an),\mathrm I(\{a\}) = (X_1 - a_1, \dots, X_n - a_n),

and this ideal is a maximal ideal of K[X1,…,Xn]K[X_1,\dots,X_n].

Formalization Note. The statement is kept in the article's setting (KK algebraically closed), although neither part needs that hypothesis.

Preamble
import Definitions.Def_Nullstellensatz_Defs
import Mathlib

open MvPolynomial
Formal statement
namespace Nullstellensatz

theorem vanishingIdeal_singleton {K : Type*} [Field K] [IsAlgClosed K] {n : ℕ}
    (a : Fin n → K) :
    vanishingIdeal {a} = pointIdeal a ∧ (pointIdeal a).IsMaximal := 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 6, first two sentences (I({a}) is a maximal ideal).
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, n∈Nn \in \mathbb N, a=(a1,…,an)∈Kna = (a_1,\dots,a_n) \in K^n. Two claims: (1) the ideal of all polynomials p∈K[X1,…,Xn]p \in K[X_1,\dots,X_n] with p(a)=0p(a) = 0 equals the ideal generated by X1−a1,…,Xn−anX_1 - a_1, \dots, X_n - a_n; (2) this ideal is maximal (proper, and no proper ideal strictly contains it). For n=0n = 0 the ideal is the zero ideal of KK.

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