Theorems · Theorem · commutative algebra

Valued.locally_const

∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {x : R},
  Valued.v x ≠ 0 → {y | Valued.v y = Valued.v x} ∈ nhds x

The set { y : R | v y = v x } is a neighbourhood of x. This does not imply that v is locally constant everywhere (since v ⁻¹' {0} is not open), but it is equivalent to the restriction of v to the complement of its support being locally constant.

Defined in

Mathlib.Topology.Algebra.Valued.ValuationTopology

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingLinearOrderedCommGroupWithZeroValued