Module

Place_exists_of_valuationSubring_of_finiteDimensional.lean

Nyll.AlgebraicCurves.Places.Place_exists_of_valuationSubring_of_finiteDimensional

1 declaration indexed from sourceView source ↗

Module documentation

Place exists of valuation Subring of finite Dimensional

Imports2

Imported by8

theorem

exists_of_valuationSubring_of_finiteDimensional

L27 ↗

AlgebraicCurve.Place.exists_of_valuationSubring_of_finiteDimensional

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_finiteDimensional
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Place.exists_of_valuationSubring_of_finiteDimensional
    {K F : Type*} [Field K] [Field F] [Algebra K F] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤) :
    ∃ v : AlgebraicCurve.Place K F, v.toValuationSubring = A

Module documentation

Place exists of valuation Subring of finite Dimensional

Declarations

exists_of_valuationSubring_of_finiteDimensional