Theorems · Theorem · commutative algebra

WithVal.equivWithVal_symm_apply

Deprecated since 2026-01-27Mathlib marks this declaration as deprecated.

∀ {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 Γ'₀) {x : WithVal w},
  (WithVal.congr v w (RingEquiv.refl R)).symm x = (WithVal.equiv v).symm ((WithVal.equiv w) x)

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