Module

Place_adicValuation_isTrivialOn.lean

Nyll.AlgebraicCurves.Places.Place_adicValuation_isTrivialOn

4 declarations indexed from sourceView source ↗

Module documentation

Place adicValuation isTrivialOn

The adic valuation of a place is trivial on the base field.

Imports1

Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by2

theorem

adicValuation_valuationSubring

L39 ↗

AlgebraicCurve.Place.adicValuation_valuationSubring

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_adicValuation_isTrivialOn
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
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.adicValuation_valuationSubring :
    v.adicValuation.valuationSubring = v.toValuationSubring

theorem

mem_iff_adicValuation_le_one

L51 ↗

AlgebraicCurve.Place.mem_iff_adicValuation_le_one

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_adicValuation_isTrivialOn
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
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_iff_adicValuation_le_one {f : F} :
    f ∈ v.toValuationSubring ↔ v.adicValuation f ≤ 1

theorem

rowMain

L57 ↗

AlgebraicCurves.Places.Proofs.Place_adicValuation_isTrivialOn.AlgebraicCurve.Place.rowMain

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_adicValuation_isTrivialOn
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
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 rowMain : v.adicValuation.IsTrivialOn K

theorem

adicValuation_isTrivialOn

L69 ↗

AlgebraicCurve.Place.adicValuation_isTrivialOn

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_adicValuation_isTrivialOn
open IsDedekindDomain WithZero IsLocalRing
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.Place_adicValuation_isTrivialOn.AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.adicValuation_isTrivialOn {K F : Type*} [Field K] [Field F]
  [Algebra K F] (v : Place K F) :
    v.adicValuation.IsTrivialOn K

Module documentation

Place adicValuation isTrivialOn

Declarations

adicValuation_valuationSubring

mem_iff_adicValuation_le_one

rowMain

adicValuation_isTrivialOn