Module

Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos.lean

Nyll.AlgebraicCurves.Places.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos

5 declarations indexed from sourceView source ↗

Module documentation

Place mem and eval At eq iff ord sub algebra Map pos

Imports2

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

ord_nonneg_of_mem

L30 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos.EvalAtAux.ord_nonneg_of_mem

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos
open AlgebraicCurve
namespace EvalAtAux
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f

theorem

ord_pos_of_mem_of_not_isUnit

L43 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos.EvalAtAux.ord_pos_of_mem_of_not_isUnit

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos
open AlgebraicCurve
namespace EvalAtAux
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_pos_of_mem_of_not_isUnit {f : F} (hf : f ∈ v.toValuationSubring) (hf0 : f ≠ 0)
    (hu : ¬ IsUnit (⟨f, hf⟩ : v.toValuationSubring)) : 0 < v.ord f

theorem

ord_eq_zero_of_isUnit

L58 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos.EvalAtAux.ord_eq_zero_of_isUnit

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos
open AlgebraicCurve
namespace EvalAtAux
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_eq_zero_of_isUnit {f : F} (hf : f ∈ v.toValuationSubring) (hu : IsUnit (⟨f, hf⟩ :
  v.toValuationSubring)) :
    v.ord f = 0

theorem

mem_of_ord_nonneg

L65 ↗

AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos.EvalAtAux.mem_of_ord_nonneg

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos
open AlgebraicCurve
namespace EvalAtAux
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_of_ord_nonneg {f : F} (h : 0 ≤ v.ord f) : f ∈ v.toValuationSubring

theorem

mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos

L90 ↗

AlgebraicCurve.Place.mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos
open AlgebraicCurve
open EvalAtAux

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : AlgebraicCurve.Place K F) (hv : v.IsRational) (f : F) (a : K) (hfa : f ≠ algebraMap K F a)
      :
    (f ∈ v.toValuationSubring ∧ v.evalAt f = a) ↔ 0 < v.ord (f - algebraMap K F a)

Module documentation

Place mem and eval At eq iff ord sub algebra Map pos

Declarations

ord_nonneg_of_mem

ord_pos_of_mem_of_not_isUnit

ord_eq_zero_of_isUnit

mem_of_ord_nonneg

mem_and_evalAt_eq_iff_ord_sub_algebraMap_pos