Zariski's lemma

Proved

Nullstellensatz.zariski_lemma

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

algebraic-geometrycommutative-algebra

Let $K$ be a field and $L$ a field which is finitely generated as an algebra over $K$ . Then $L$ is a finite extension of $K$ :

\dim_K L < \infty.

Zariski's lemma is the algebraic input for the proof of the weak Nullstellensatz via maximal ideals.

Preamble

import Definitions.Def_Nullstellensatz_Defs
import Mathlib

open MvPolynomial

Formal statement

namespace Nullstellensatz

theorem zariski_lemma {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.FiniteType K L] :
    Module.Finite K L := 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 "Proofs", subsection "Using Zariski's lemma", first sentence.

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 $K$ and $L$ be fields with a $K$ -algebra structure on $L$ , and assume $L$ is finitely generated as a $K$ -algebra (there are finitely many elements of $L$ such that every element is a polynomial expression in them with coefficients from $K$ ). Then $L$ is finitely generated as a $K$ -vector space (a $K$ -module).

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