Module

Place_finite_setOf_not_mem_toValuationSubring_or_evalAt_mem.lean

Nyll.AlgebraicCurves.Places.Place_finite_setOf_not_mem_toValuationSubring_or_evalAt_mem

4 declarations indexed from sourceView source ↗

Module documentation

Place finite set Of not mem to Valuation Subring or eval At mem

Imports1

Nyll.AlgebraicCurves.Places.Evaluation

Imported by2

theorem

fov_ord_coe_eq_zero_iff

L34 ↗

AlgebraicCurve.Place.fov_ord_coe_eq_zero_iff

Source context 10 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.fov_ord_coe_eq_zero_iff (v : Place K F) (a :
  v.toValuationSubring) (ha : (a : F) ≠ 0) :
    v.ord (a : F) = 0 ↔ IsUnit a

theorem

fov_ord_ne_zero_of_not_mem

L49 ↗

AlgebraicCurve.Place.fov_ord_ne_zero_of_not_mem

Source context 11 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.fov_ord_ne_zero_of_not_mem (v : Place K F) {x : F} (hx
  : x ∉ v.toValuationSubring) : v.ord x ≠ 0

theorem

fov_ord_sub_ne_zero_of_evalAt_eq

L75 ↗

AlgebraicCurve.Place.fov_ord_sub_ne_zero_of_evalAt_eq

Source context 12 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.fov_ord_sub_ne_zero_of_evalAt_eq (v : Place K F) (hv :
  v.IsRational) {x : F}
    (hx : x ∉ Set.range (algebraMap K F)) (hmem : x ∈ v.toValuationSubring) {t : K} (ht : v.evalAt
      x = t) :
    v.ord (x - algebraMap K F t) ≠ 0

theorem

finite_setOf_not_mem_toValuationSubring_or_evalAt_mem

L99 ↗

AlgebraicCurve.Place.finite_setOf_not_mem_toValuationSubring_or_evalAt_mem

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_finite_setOf_not_mem_toValuationSubring_or_evalAt_mem
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Place.finite_setOf_not_mem_toValuationSubring_or_evalAt_mem
    {K F : Type*} [Field K] [Field F] [Algebra K F] [HasPrincipalDivisors K F]
    (hrat : ∀ v : Place K F, v.IsRational)
    (x : F) (hx : x ∉ Set.range (algebraMap K F)) (T : Finset K) :
    {v : Place K F | x ∉ v.toValuationSubring ∨ v.evalAt x ∈ (T : Set K)}.Finite

Module documentation

Place finite set Of not mem to Valuation Subring or eval At mem

Declarations

fov_ord_coe_eq_zero_iff

fov_ord_ne_zero_of_not_mem

fov_ord_sub_ne_zero_of_evalAt_eq

finite_setOf_not_mem_toValuationSubring_or_evalAt_mem