NYLL
Module

Place_hasValue_iff_mem_and_eq_or_ord_sub_pos.lean

Nyll.AlgebraicCurves.Places.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
11 declarations indexed from sourceView source ↗

Module documentation

Place has Value iff mem and eq or ord sub pos

Imports1
Imported by1

Declarations

theorem

ord_nonneg_of_mem_e15

L35 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem_e15
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
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.ord_nonneg_of_mem_e15 {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg_e15

L53 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg_e15
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
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.mem_of_ord_nonneg_e15 {f : F} (hf : f ≠ 0) (h : 0 ≤
  v.ord f) :
    f ∈ v.toValuationSubring
theorem

ord_algebraMap_e15

L64 ↗
AlgebraicCurve.Place.ord_algebraMap_e15
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
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.ord_algebraMap_e15 (c : K) : v.ord (algebraMap K F c) =
  0
theorem

ne_zero_of_ord_pos_e15

L72 ↗
AlgebraicCurve.Place.ne_zero_of_ord_pos_e15
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
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.ne_zero_of_ord_pos_e15 {f : F} (h : 0 < v.ord f) : f ≠
  0
theorem

isUnit_iff_ord_eq_zero_e15

L79 ↗
AlgebraicCurve.Place.isUnit_iff_ord_eq_zero_e15
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
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.isUnit_iff_ord_eq_zero_e15 {f : F} (hf : f ∈
  v.toValuationSubring) (hf0 : f ≠ 0) :
    IsUnit (⟨f, hf⟩ : v.toValuationSubring) ↔ v.ord f = 0
theorem

hasValue_iff_eq_or_ord_sub_pos_e15

L92 ↗
AlgebraicCurve.Place.hasValue_iff_eq_or_ord_sub_pos_e15
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
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.hasValue_iff_eq_or_ord_sub_pos_e15 {g : F} (hg : g ∈
  v.toValuationSubring) (c : K) :
    v.HasValue g c ↔ g = algebraMap K F c ∨ 0 < v.ord (g - algebraMap K F c)
theorem

div_mem_of_ord_le_e15

L122 ↗
AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos.AlgebraicCurve.Place.div_mem_of_ord_le_e15
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
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 div_mem_of_ord_le_e15 {r t : F} (ht : t ≠ 0) (h : v.ord t ≤ v.ord r) :
    r / t ∈ v.toValuationSubring
theorem

tExpansion_coeff_unique_e15

L130 ↗
AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos.AlgebraicCurve.Place.tExpansion_coeff_unique_e15
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
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 tExpansion_coeff_unique_e15 {t : F} (ht : 0 < v.ord t) (r : F) (c c' : ℕ → K)
    (hc : ∀ m : ℕ, (r - ∑ i ∈ Finset.range m, algebraMap K F (c i) * t ^ i) / t ^ m ∈
      v.toValuationSubring)
    (hc' : ∀ m : ℕ, (r - ∑ i ∈ Finset.range m, algebraMap K F (c' i) * t ^ i) / t ^ m ∈
      v.toValuationSubring) :
    c = c'
theorem

inv_mem_of_isUnit_e15

L179 ↗
Subring.inv_mem_of_isUnit_e15
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace Subring
open scoped _root_.Subring in
Lean source · statement
theorem _root_.Subring.inv_mem_of_isUnit_e15 {F : Type*} [Field F] {S : Subring F} {t : F}
  (h : t ∈ S)
    (hu : IsUnit (⟨t, h⟩ : S)) : t⁻¹ ∈ S
theorem

inv_mem_of_isUnit_e15

L196 ↗
ValuationSubring.inv_mem_of_isUnit_e15
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
namespace ValuationSubring
open scoped _root_.ValuationSubring in
Lean source · statement
theorem _root_.ValuationSubring.inv_mem_of_isUnit_e15 {F : Type*} [Field F] {S :
  ValuationSubring F} {t : F}
    (h : t ∈ S) (hu : IsUnit (⟨t, h⟩ : S)) : t⁻¹ ∈ S
theorem

hasValue_iff_mem_and_eq_or_ord_sub_pos

L209 ↗
AlgebraicCurve.Place.hasValue_iff_mem_and_eq_or_ord_sub_pos
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_hasValue_iff_mem_and_eq_or_ord_sub_pos
open _root_.AlgebraicCurve
open _root_.IsLocalRing
Lean source · statement
theorem _root_.AlgebraicCurve.Place.hasValue_iff_mem_and_eq_or_ord_sub_pos
    {K L : Type*} [Field K] [Field L] [Algebra K L] (v : Place K L) (g : L) (c : K) :
    v.HasValue g c ↔
      g ∈ v.toValuationSubring ∧ (g = algebraMap K L c ∨ 0 < v.ord (g - algebraMap K L c))

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