NYLL
Module

Place_exists_forall_ord_eq_finset.lean

Nyll.AlgebraicCurves.Places.Place_exists_forall_ord_eq_finset
10 declarations indexed from sourceView source ↗

Module documentation

Place exists forall ord eq finset

Weak approximation constructs a nonzero function with prescribed integer orders at a finite set of places.

Imports4
Imported by5

Declarations

theorem

ord_neg_impl

L42 ↗
AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve.WC1bSolAW.ord_neg_impl
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolAW
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_neg_impl (v : Place K F) (f : F) : v.ord (-f) = v.ord f
theorem

add_ne_zero_of_ord_lt

L45 ↗
AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve.WC1bSolAW.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_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolAW
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem add_ne_zero_of_ord_lt (v : Place K F) {f g : F} (hlt : v.ord f < v.ord g) :
    f + g ≠ 0
theorem

ord_add_eq_of_ord_lt

L51 ↗
AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve.WC1bSolAW.ord_add_eq_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_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolAW
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_add_eq_of_ord_lt (v : Place K F) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0)
    (hlt : v.ord f < v.ord g) : v.ord (f + g) = v.ord f
theorem

ord_lt_zero_of_notMem

L60 ↗
AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve.WC1bSolAW.ord_lt_zero_of_notMem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolAW
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_lt_zero_of_notMem (v : Place K F) {f : F} (hf : f ≠ 0) (h : f ∉ v.toValuationSubring) :
    v.ord f < 0
theorem

exists_mem_notMem_of_ne

L65 ↗
AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve.WC1bSolAW.exists_mem_notMem_of_ne
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolAW
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_mem_notMem_of_ne {v w : Place K F} (hvw : v ≠ w) :
    ∃ x : F, x ≠ 0 ∧ x ∈ v.toValuationSubring ∧ x ∉ w.toValuationSubring
theorem

exists_ord_pos_ord_neg_of_ne

L72 ↗
AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve.WC1bSolAW.exists_ord_pos_ord_neg_of_ne
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolAW
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_ord_pos_ord_neg_of_ne {v w : Place K F} (hvw : v ≠ w) :
    ∃ z : F, z ≠ 0 ∧ 0 < v.ord z ∧ w.ord z < 0
theorem

ord_finsetSum_gt

L87 ↗
AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve.WC1bSolAW.ord_finsetSum_gt
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolAW
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_finsetSum_gt {ι : Type*} (v : Place K F) (s : Finset ι) (g : ι → F) (m : ℤ) :
    (∀ i ∈ s, g i ≠ 0 ∧ m < v.ord (g i)) →
      s.sum g = 0 ∨ (s.sum g ≠ 0 ∧ m < v.ord (s.sum g))
theorem

exists_separating

L105 ↗
AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve.WC1bSolAW.exists_separating
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolAW
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_separating (v : Place K F) (S : Finset (Place K F)) :
    ∃ t : F, t ≠ 0 ∧ 0 < v.ord t ∧ ∀ w ∈ S, w ≠ v → w.ord t < 0
theorem

exists_forall_ord_eq_finset

L180 ↗
AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve.WC1bSolAW.exists_forall_ord_eq_finset
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC1bSolAW
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_forall_ord_eq_finset (S : Finset (Place K F)) (n : Place K F → ℤ) :
    ∃ g : F, g ≠ 0 ∧ ∀ v ∈ S, v.ord g = n v
theorem

exists_forall_ord_eq_finset

L292 ↗
AlgebraicCurve.Place.exists_forall_ord_eq_finset
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.Place_exists_forall_ord_eq_finset.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_forall_ord_eq_finset {K F : Type*} [Field K]
  [Field F] [Algebra K F] (S : Finset (AlgebraicCurve.Place K F)) (n :
  AlgebraicCurve.Place K F → ℤ) :
    ∃ g : F, g ≠ 0 ∧ ∀ v ∈ S, v.ord g = n v

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