Theorems · Inductive type · number theory

IsNonarchimedeanLocalField

(K : Type u_1) → [inst : Field K] → [ValuativeRel K] → [TopologicalSpace K] → Prop

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

Cited by

1 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

FieldValuativeRelTopologicalSpace