Theorems · Theorem · field theory

Valued.integer.mem_iff

∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] {x : K},
  x ∈ Valued.integer K ↔ ‖x‖ ≤ 1

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.

Defined in

Mathlib.Topology.Algebra.Valued.LocallyCompact

Cited by

1 results in Mathlib

Foundations

Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldIsUltrametricDist