Theorems · Theorem · commutative algebra

Valuation.cauchy_iff

∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_u : UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible]
  {F : Filter R},
  Cauchy F ↔
    F.NeBot ∧ ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

Defined in

Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingValuativeRelLinearOrderedCommGroupWithZeroUniformSpaceIsUniformAddGroupIsValuativeTopologyValuation.Compatible