Documentation

Mathlib.Topology.Algebra.Valued.LocallyCompact

Necessary and sufficient conditions for a locally compact nonarchimedean normed field #

Main Definitions #

Tags #

norm, nonarchimedean, rank one, compact, locally compact

An element is in the valuation ring if the norm is bounded by 1. This is a variant of Valuation.mem_integer_iff, phrased using norms instead of the valuation.

@[simp]
theorem Valued.integer.isPrincipalIdealRing_of_compactSpace {F : Type u_2} {Γ₀ : Type u_3} [Field F] [LinearOrderedCommGroupWithZero Γ₀] [MulArchimedean Γ₀] [hv : Valued F Γ₀] [CompactSpace (integer F)] (h : ∃ (x : F), 0 < v x v x < 1) :