Structures · Algebra

IsNonarchimedeanLocalField

Given a topological field K equipped with an equivalence class of valuations (a ValuativeRel), we say that it is a non-archimedean local field if the topology comes from the given valuation, and it is locally compact and non-discrete. This implies the following typeclasses via inferInstance - IsValuativeTopology K - LocallyCompactSpace K - IsTopologicalDivisionRing K - ValuativeRel.IsNontrivial K - ValuativeRel.IsRankLeOne K - ValuativeRel.IsDiscrete K - IsDiscreteValuationRing 𝒪[K] - Finite 𝓀[K] Assuming we have a compatible UniformSpace K instance (e.g. via IsTopologicalAddGroup.toUniformSpace and isUniformAddGroup_of_addCommGroup) then - CompleteSpace K - CompleteSpace 𝒪[K]

Defined in

Mathlib.NumberTheory.LocalField.Basic

Shape

One type argument