Theorems · Theorem · commutative algebra

Valuation.isEquiv_tfae

∀ {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 y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1,
      ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZero