NYLL
Module

FinitelyGeneratedMixedCharacteristic.lean

Nyll.AlgebraicCurves.Valuations.FinitelyGeneratedMixedCharacteristic
2 declarations indexed from sourceView source ↗

Module documentation

Mixed-characteristic discrete valuations on finitely generated fields

Imports5
Imported by2

Declarations

theorem

exists_discreteValuationSubring_prime_nonunit_of_fg

L22 ↗
FieldTheory.exists_discreteValuationSubring_prime_nonunit_of_fg
Documentation

A finitely generated field of characteristic zero admits a discrete valuation ring in which some prime number is a nonunit.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldTheory
universe u
Lean source · statement
theorem exists_discreteValuationSubring_prime_nonunit_of_fg
    (K : Type u) [Field K] [CharZero K] (hfg : Field.FG K) :
    ∃ p : ℕ, p.Prime ∧ ∃ V : ValuationSubring K,
      IsDiscreteValuationRing V ∧ (p : K) ∈ V.nonunits
theorem

exists_mixedChar_DVF_of_fg

L63 ↗
FieldTheory.exists_mixedChar_DVF_of_fg
Documentation

A finitely generated characteristic-zero field admits an actual mixed-characteristic discrete valuation, with integer value group.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldTheory
universe u
Lean source · statement
theorem exists_mixedChar_DVF_of_fg
    (K : Type u) [Field K] [CharZero K] (hfg : Field.FG K) :
    ∃ p : ℕ, p.Prime ∧ ∃ D : ValuationTheory.DiscreteValuationField.DVF.{u, 0} K,
      CharP D.residueField p

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.