NYLL
Module

Place_exists_ord_algebraMap_eq_mul_ord.lean

Nyll.AlgebraicCurves.Places.Place_exists_ord_algebraMap_eq_mul_ord
6 declarations indexed from sourceView source ↗

Module documentation

Place exists ord algebra Map eq mul ord

Imports1
Imported by3

Declarations

theorem

ord_nonneg_of_mem'

L39 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsOrdAlgebraMapMulOrd
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
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' {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg'

L56 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg'
Source context 13 commands

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

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

mem_iff_ord_nonneg'

L66 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsOrdAlgebraMapMulOrd.AlgebraicCurve.Place.mem_iff_ord_nonneg'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsOrdAlgebraMapMulOrd
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
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 mem_iff_ord_nonneg' {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f
theorem

exists_ord_pos_mem'

L70 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsOrdAlgebraMapMulOrd.AlgebraicCurve.Place.exists_ord_pos_mem'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsOrdAlgebraMapMulOrd
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
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 exists_ord_pos_mem' : ∃ f : F, f ≠ 0 ∧ 0 < v.ord f ∧ f ∈ v.toValuationSubring
theorem

rowMain

L83 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsOrdAlgebraMapMulOrd.AlgebraicCurve.Place.rowMain
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsOrdAlgebraMapMulOrd
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Fiber
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
Lean source · statement
theorem rowMain (w : Place K F') (v : Place K F)
    (hv : v.toValuationSubring = w.toValuationSubring.comap (algebraMap F F')) :
    ∃ e : ℕ, 0 < e ∧ ∀ f : F, w.ord (algebraMap F F' f) = e * v.ord f
theorem

exists_ord_algebraMap_eq_mul_ord

L151 ↗
AlgebraicCurve.Place.exists_ord_algebraMap_eq_mul_ord
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsOrdAlgebraMapMulOrd
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.PlaceExistsOrdAlgebraMapMulOrd.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_algebraMap_eq_mul_ord {K F F' : Type*} [Field K]
  [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] (w : Place K F') (v : Place K
  F) (hv : v.toValuationSubring = w.toValuationSubring.comap (algebraMap F F')) :
    ∃ e : ℕ, 0 < e ∧ ∀ f : F, w.ord (algebraMap F F' f) = e * v.ord f

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