Theorems · Theorem · commutative algebra

WithVal.equivWithVal_symm

Deprecated since 2026-01-27Use WithVal.congr_symm instead.

∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {Γ'₀ : Type u_3}
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation R Γ₀) (w : Valuation R Γ'₀),
  (WithVal.congr v w (RingEquiv.refl R)).symm = WithVal.congr w v (RingEquiv.refl R)

Defined in

Mathlib.Topology.Algebra.Valued.WithVal

Cited by

0 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

LinearOrderedCommGroupWithZeroRingLinearOrderedCommGroupWithZero