Theorems · Theorem · commutative algebra

Valuation.IsEquiv.valuedCompletion_le_one_iff

∀ {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ₀'] {K : Type u_7} [inst_2 : Field K] {v : Valuation K Γ₀}
  {w : Valuation K Γ₀'} (h : v.IsEquiv w) {x : v.Completion},
  Valued.v x ≤ 1 ↔ Valued.v ((UniformSpace.Completion.mapEquiv h.uniformEquiv) x) ≤ 1

Defined in

Mathlib.Topology.Algebra.Valued.WithVal

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZeroField