Theorems · Theorem · commutative algebra

Valuation.locally_const

∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_3 : TopologicalSpace R] (v : Valuation R Γ₀) [v.Compatible] [IsValuativeTopology R] {x : R},
  v x ≠ 0 → {y | v y = 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.ValuativeRel.ValuativeTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingValuativeRelLinearOrderedCommGroupWithZeroTopologicalSpaceValuation.CompatibleIsValuativeTopology