Theorems · Theorem · commutative algebra

Valuation.IsEquiv.val_eq

Deprecated since 2026-03-05Use Valuation.IsEquiv.eq_iff instead.

∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {r s : R}, v₁ r = v₁ s ↔ v₂ r = v₂ s

Alias of Valuation.IsEquiv.eq_iff.

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext

Assumes

RingLinearOrderedCommMonoidWithZeroLinearOrderedCommMonoidWithZero