Theorems · Theorem · commutative algebra

WithVal.equiv_apply

∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (self : WithVal v), (WithVal.equiv v) self = self.ofVal

Defined in

Mathlib.Topology.Algebra.Valued.WithVal

Cited by

6 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

LinearOrderedCommGroupWithZeroRing