Module

AddVal.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.AddVal

2 declarations indexed from sourceView source ↗

Module documentation

Normalized additive valuations on discrete valuation rings

This file supplies general-purpose facts about Mathlib's normalized additive valuation on a discrete valuation ring which are independent of any chosen valued-field presentation.

Imports1

Mathlib.RingTheory.DiscreteValuationRing.Basic

Imported by12

theorem

mem_maximalIdeal_pow_iff_addVal_ge

L29 ↗

IsDiscreteValuationRing.mem_maximalIdeal_pow_iff_addVal_ge

Documentation

Membership in a power of the maximal ideal is detected by the normalized additive valuation.

Source context 4 commands

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

noncomputable section
universe u
namespace IsDiscreteValuationRing
variable {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]

Lean source · statement

theorem mem_maximalIdeal_pow_iff_addVal_ge (a : R) (n : ℕ) :
    a ∈ IsLocalRing.maximalIdeal R ^ n ↔ (n : ℕ∞) ≤ addVal R a

theorem

addVal_ringEquiv

L37 ↗

IsDiscreteValuationRing.addVal_ringEquiv