Local uniformization

Theorem · local_uniformization_of_charZero

**Zariski's local uniformization theorem.** Every valuation ring of a finitely generated field extension $F \mid k$ that contains a field $k$ of characteristic zero admits local uniformization over $k$ . This is the main theorem of [Zar1940].

Formal statement · Lean 4.lean

theorem local_uniformization_of_charZero (k F : Type*) [Field k] [Field F] [Algebra k F]
    [Algebra.EssFiniteType k F] [CharZero k] (𝒪 : ValuationSubring F)
    (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) :
    𝒪.HasLocalUniformization k := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗