Theorems · Definition · commutative algebra

Valuation.IsEquiv.uniformEquiv

{R : Type u_4} →
  {Γ₀ : Type u_5} →
    {Γ₀' : Type u_6} →
      [inst : Ring R] →
        [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
          [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] →
            {v : Valuation R Γ₀} → {w : Valuation R Γ₀'} → v.IsEquiv w → WithVal v ≃ᵤ WithVal w

If two valuations v and w are equivalent then WithVal v and WithVal w are isomorphic as uniform spaces.

Defined in

Mathlib.Topology.Algebra.Valued.WithVal

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingLinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZero