NYLL
Module

Place_exists_forall_ord_eq.lean

Nyll.AlgebraicCurves.Places.Place_exists_forall_ord_eq
16 declarations indexed from sourceView source ↗

Module documentation

Place exists forall ord eq

Imports1
Imported by7

Declarations

theorem

mem_iff_adicValuation_le_one'

L38 ↗
AlgebraicCurve.Place.mem_iff_adicValuation_le_one'
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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.mem_iff_adicValuation_le_one' (x : F) :
    x ∈ v.toValuationSubring ↔ v.adicValuation x ≤ 1
theorem

adicValuation_eq_exp_neg_ord

L70 ↗
AlgebraicCurve.Place.adicValuation_eq_exp_neg_ord
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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.adicValuation_eq_exp_neg_ord {x : F} (hx : x ≠ 0) :
    v.adicValuation x = WithZero.exp (-v.ord x)
theorem

mem_iff_ord_nonneg'

L76 ↗
AlgebraicCurve.Place.mem_iff_ord_nonneg'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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.mem_iff_ord_nonneg' {x : F} (hx : x ≠ 0) :
    x ∈ v.toValuationSubring ↔ 0 ≤ v.ord x
theorem

not_mem_iff_ord_neg

L83 ↗
AlgebraicCurve.Place.not_mem_iff_ord_neg
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.not_mem_iff_ord_neg (x : F) : x ∉ v.toValuationSubring
  ↔ v.ord x < 0
theorem

adicValuation_lt_one_iff_ord_pos

L91 ↗
AlgebraicCurve.Place.adicValuation_lt_one_iff_ord_pos
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.adicValuation_lt_one_iff_ord_pos {x : F} (hx : x ≠ 0) :
    v.adicValuation x < 1 ↔ 0 < v.ord x
theorem

one_lt_adicValuation_iff_ord_neg

L96 ↗
AlgebraicCurve.Place.one_lt_adicValuation_iff_ord_neg
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.one_lt_adicValuation_iff_ord_neg {x : F} (hx : x ≠ 0) :
    1 < v.adicValuation x ↔ v.ord x < 0
theorem

adicValuation_le_exp_neg_iff_le_ord

L101 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd.AlgebraicCurve.Place.adicValuation_le_exp_neg_iff_le_ord
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem adicValuation_le_exp_neg_iff_le_ord {x : F} (hx : x ≠ 0) (N : ℤ) :
    v.adicValuation x ≤ WithZero.exp (-N) ↔ N ≤ v.ord x
theorem

ord_coe_unit_eq_zero_of_le

L105 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd.AlgebraicCurve.Place.ord_coe_unit_eq_zero_of_le
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_coe_unit_eq_zero_of_le {v w : Place K F}
    (h : v.toValuationSubring ≤ w.toValuationSubring) (u : v.toValuationSubringˣ) :
    w.ord ((u : v.toValuationSubring) : F) = 0
theorem

exists_mem_and_not_mem

L123 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd.AlgebraicCurve.Place.exists_mem_and_not_mem
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem exists_mem_and_not_mem {v w : Place K F} (hvw : v ≠ w) :
    ∃ x : F, x ∈ v.toValuationSubring ∧ x ∉ w.toValuationSubring
theorem

exists_ord_neg_and_ord_pos

L161 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd.AlgebraicCurve.Place.exists_ord_neg_and_ord_pos
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem exists_ord_neg_and_ord_pos {v w : Place K F} (hvw : v ≠ w) :
    ∃ a : F, v.ord a < 0 ∧ 0 < w.ord a
theorem

one_add_ne_zero_and_ord_eq_of_ord_neg

L177 ↗
AlgebraicCurve.Place.one_add_ne_zero_and_ord_eq_of_ord_neg
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.one_add_ne_zero_and_ord_eq_of_ord_neg {t : F} (ht :
  v.ord t < 0) :
    1 + t ≠ 0 ∧ v.ord (1 + t) = v.ord t
theorem

ord_one_add_of_ord_pos

L197 ↗
AlgebraicCurve.Place.ord_one_add_of_ord_pos
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_one_add_of_ord_pos {t : F} (ht : 0 < v.ord t) :
    v.ord (1 + t) = 0
theorem

exists_ord_neg_forall_ord_pos

L211 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd.AlgebraicCurve.Place.exists_ord_neg_forall_ord_pos
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem exists_ord_neg_forall_ord_pos (T : Finset (Place K F)) {v : Place K F}
    (hv : v ∉ T) :
    ∃ z : F, v.ord z < 0 ∧ ∀ w ∈ T, 0 < w.ord z
theorem

exists_indicator

L287 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd.AlgebraicCurve.Place.exists_indicator
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem exists_indicator (T : Finset (Place K F)) {v : Place K F} {z : F} (hzv : v.ord z < 0)
    (hzT : ∀ w ∈ T, w ≠ v → 0 < w.ord z) (N : ℤ) :
    ∃ e : F, v.adicValuation (e - 1) ≤ WithZero.exp (-N) ∧
      ∀ w ∈ T, w ≠ v → w.adicValuation e ≤ WithZero.exp (-N)
theorem

exists_forall_ord_eq_of_sep

L325 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd.AlgebraicCurve.Place.exists_forall_ord_eq_of_sep
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem exists_forall_ord_eq_of_sep (T : Finset (Place K F)) (n : Place K F → ℤ)
    (hsep : ∀ v ∈ T, ∃ z : F, v.ord z < 0 ∧ ∀ w ∈ T, w ≠ v → 0 < w.ord z) :
    ∃ f : F, f ≠ 0 ∧ ∀ v ∈ T, v.ord f = n v
theorem

exists_forall_ord_eq

L413 ↗
AlgebraicCurve.Place.exists_forall_ord_eq
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsAllOrd
open _root_.AlgebraicCurves.Places.Proofs
open IsDedekindDomain
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_forall_ord_eq {K F : Type*} [Field K] [Field F]
  [Algebra K F]
    (T : Finset (Place K F)) (n : Place K F → ℤ) :
    ∃ f : F, f ≠ 0 ∧ ∀ v ∈ T, v.ord f = n v

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