Module

Place_exists_forall_adicValuation_sub_le.lean

Nyll.AlgebraicCurves.Places.Place_exists_forall_adicValuation_sub_le

5 declarations indexed from sourceView source ↗

Module documentation

Place exists forall adicValuation sub le

Weak approximation constructs a function whose adic distance from prescribed values is bounded at finitely many places.

Imports6

Imported by2

theorem

wa_add_ne_zero_of_ord_lt

L41 ↗

AlgebraicCurve.Place.wa_add_ne_zero_of_ord_lt

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_adicValuation_sub_le
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.wa_add_ne_zero_of_ord_lt {f g : F} (hlt :
  v.ord f < v.ord g) : f + g ≠ 0

theorem

wa_min_ord_le_ord_add

L49 ↗

AlgebraicCurve.Place.wa_min_ord_le_ord_add

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_adicValuation_sub_le
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.wa_min_ord_le_ord_add {f g : F} (hfg : f + g ≠ 0) :
    min (v.ord f) (v.ord g) ≤ v.ord (f + g)

theorem

wa_exists_separating_finset

L59 ↗

AlgebraicCurves.Places.Proofs.Place_exists_forall_adicValuation_sub_le.AlgebraicCurve.Place.wa_exists_separating_finset

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_adicValuation_sub_le
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem wa_exists_separating_finset (T : Finset (Place K F)) :
    ∃ t : F, t ≠ 0 ∧ v.ord t = 1 ∧ ∀ w ∈ T, w ≠ v → w.ord t = -1

theorem

wa_ord_finsetSum_ge

L68 ↗

AlgebraicCurve.Place.wa_ord_finsetSum_ge

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_adicValuation_sub_le
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.wa_ord_finsetSum_ge {ι : Type*} (s : Finset ι)
    (g : ι → F) (m : ℤ) (hbound : ∀ i ∈ s, g i = 0 ∨ m ≤ v.ord (g i)) :
    s.sum g = 0 ∨ m ≤ v.ord (s.sum g)

theorem

exists_forall_adicValuation_sub_le

L94 ↗

AlgebraicCurve.Place.exists_forall_adicValuation_sub_le

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_le
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.Place_exists_forall_adicValuation_sub_le.AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.exists_forall_adicValuation_sub_le {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 le

Declarations

wa_add_ne_zero_of_ord_lt

wa_min_ord_le_ord_add

wa_exists_separating_finset

wa_ord_finsetSum_ge

exists_forall_adicValuation_sub_le