Module

Place_adicValuation_isRankOneDiscrete.lean

Nyll.AlgebraicCurves.Places.Place_adicValuation_isRankOneDiscrete

2 declarations indexed from sourceView source ↗

Module documentation

Place adicValuation isRankOneDiscrete

The adic valuation attached to a place is discrete of rank one.

Imports1

Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by2

theorem

rowMain

L39 ↗

AlgebraicCurves.Places.Proofs.Place_adicValuation_isRankOneDiscrete.AlgebraicCurve.Place.rowMain

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_adicValuation_isRankOneDiscrete
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 rowMain : v.adicValuation.IsRankOneDiscrete

theorem

adicValuation_isRankOneDiscrete

L50 ↗

AlgebraicCurve.Place.adicValuation_isRankOneDiscrete

Source context 4 commands