Theorems · Theorem · commutative algebra

Valuation.isEquiv_iff_val_sub_one_lt_one

∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀},
  v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZero