Theorems · Theorem · commutative algebra

Valuation.is_topological_valuation

∀ {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] (s : Set R),
  s ∈ nhds 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s

Alias of Valuation.mem_nhds_zero_iff.

Defined in

Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingValuativeRelLinearOrderedCommGroupWithZeroTopologicalSpaceValuation.CompatibleIsValuativeTopology