Theorems · Theorem · field theory

Valued.closure_coe_completion_v_mul_v_lt

∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  {r s : K},
  r ≠ 0 →
    s ≠ 0 →
      closure (UniformSpace.Completion.coe' '' {x | Valued.v x * Valued.v r < Valued.v s}) =
        {x | Valued.extensionValuation x * Valued.v r < Valued.v s}

Defined in

Mathlib.Topology.Algebra.Valued.ValuedField

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderedCommGroupWithZeroValued