Module

Place_exists_forall_adicValuation_sub_eq.lean

Nyll.AlgebraicCurves.Places.Place_exists_forall_adicValuation_sub_eq

1 declaration indexed from sourceView source ↗

Module documentation

Place exists forall adicValuation sub eq

Weak approximation realizes prescribed nonzero adic distances from given values at finitely many places.

Imports6

Imported by3

theorem

exists_forall_adicValuation_sub_eq

L32 ↗

AlgebraicCurve.Place.exists_forall_adicValuation_sub_eq

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_adicValuation_sub_eq
open AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.exists_forall_adicValuation_sub_eq {K F : Type*} [Field K]
  [Field F] [Algebra K F]
    (T : Finset (AlgebraicCurve.Place K F)) (β : AlgebraicCurve.Place K F → F)
    (n : AlgebraicCurve.Place K F → ℤ) :
    ∃ f : F, ∀ v ∈ T, v.adicValuation (f - β v) = WithZero.exp (n v)

Module documentation

Place exists forall adicValuation sub eq

Declarations

exists_forall_adicValuation_sub_eq