Module

WithZeroCompleteSpace.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.WithZeroCompleteSpace

1 declaration indexed from sourceView source ↗

Module documentation

Completeness for the actual topology of an integer-valued DVF

The valuation ring is complete in its native subtype topology because that topology is maximal-ideal adic. A compatible norm identifies this ring with the closed unit ball, whose completeness implies completeness of the field. The norm retains the original valuation uniformity. No residue-field finiteness or local compactness is required.

Imports5

Nyll.ValuedFieldTheory.Valuation.ValuedAdicComplete
Mathlib.Analysis.Normed.Field.Lemmas
Mathlib.RingTheory.AdicCompletion.Topology
Mathlib.RingTheory.Valuation.Discrete.RankOne
Mathlib.Topology.Algebra.Valued.NormedValued

Imported by3

theorem

completeSpace_ofWithZeroValuation

L29 ↗

ValuationTheory.DiscreteValuationField.Valuation.completeSpace_ofWithZeroValuation

Documentation

Adic completeness of an integer-valued discrete valuation supplies completeness for the actual uniformity induced by that valuation.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField.Valuation
variable {K : Type*} [Field K]

Lean source · statement

theorem completeSpace_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) [IsCompleteDiscrete v] :
    @CompleteSpace K (Valued.mk' v).toUniformSpace

Module documentation

Completeness for the actual topology of an integer-valued DVF

Declarations

completeSpace_ofWithZeroValuation