Module

Place_exists_ord_eq_one_of_ord_sum_eq_one.lean

Nyll.AlgebraicCurves.Places.Place_exists_ord_eq_one_of_ord_sum_eq_one

3 declarations indexed from sourceView source ↗

Module documentation

Place exists ord eq one of ord sum eq one

Imports1

Nyll.AlgebraicCurves.Places.Evaluation

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

c3a_adicValuation_le_exp_neg_iff

L36 ↗

AlgebraicCurve.Place.c3a_adicValuation_le_exp_neg_iff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_ord_eq_one_of_ord_sum_eq_one
open _root_.AlgebraicCurve
open _root_.Polynomial
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] (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.c3a_adicValuation_le_exp_neg_iff (f : F) (n : ℤ) :
    v.adicValuation f ≤ WithZero.exp (-n) ↔ f = 0 ∨ n ≤ v.ord f

theorem

c3a_adicValuation_algebraMap_le_one

L47 ↗

AlgebraicCurve.Place.c3a_adicValuation_algebraMap_le_one

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_ord_eq_one_of_ord_sum_eq_one
open _root_.AlgebraicCurve
open _root_.Polynomial
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] (v : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.c3a_adicValuation_algebraMap_le_one (c : K) :
  v.adicValuation (algebraMap K F c) ≤ 1

theorem

exists_ord_eq_one_of_ord_sum_eq_one

L57 ↗

AlgebraicCurve.Place.exists_ord_eq_one_of_ord_sum_eq_one

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_ord_eq_one_of_ord_sum_eq_one
open _root_.AlgebraicCurve
open _root_.Polynomial

Lean source · statement

theorem _root_.AlgebraicCurve.Place.exists_ord_eq_one_of_ord_sum_eq_one
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) {ι : Type*} (s : Finset ι) (c : ι → K) (f : ι → F)
    (hf : ∀ i ∈ s, f i = 0 ∨ 1 ≤ v.ord (f i))
    (h : v.ord (∑ i ∈ s, algebraMap K F (c i) * f i) = 1) :
    ∃ i ∈ s, v.ord (f i) = 1

Module documentation

Place exists ord eq one of ord sum eq one

Declarations

c3a_adicValuation_le_exp_neg_iff

c3a_adicValuation_algebraMap_le_one

exists_ord_eq_one_of_ord_sum_eq_one