Local uniformization

Exercise · hasLocalUniformization_top

The trivial valuation subring of a function field is uniformized by any affine model, since its centre is the generic point.

Formal statement · Lean 4.lean

theorem hasLocalUniformization_top {F : Type*} [Field F] {k : Type*} [Field k] [Algebra k F]
    (A : Subalgebra k F) [Algebra.FiniteType k A] [IsFractionRing A F] :
    (⊤ : ValuationSubring F).HasLocalUniformization k := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗