Theorems · Theorem · commutative algebra

Valuation.ofAddValuation_apply

∀ {R : Type u_3} {Γ₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : AddValuation R (Additive Γ₀)ᵒᵈ) (r : R), (Valuation.ofAddValuation v) r = Additive.toMul (OrderDual.ofDual (v r))

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingLinearOrderedCommMonoidWithZero