toAddValuation_apply — Mathlib

English

The value of the AddValuation corresponding to v at r is the dual of v(r), interpreted in Additive Γ0.

Русский

Значение AddValuation, соответствующего v, в точке r равно двойственному значению v(r), воспринятому в Additive Γ0.

LaTeX

$$$ (toAddValuation v)(r) = \\mathrm{OrderDual}.toDual(\\mathrm{Additive}.ofMul(v(r))). $$$

Lean4

@[simp]
theorem toAddValuation_apply (v : Valuation R Γ₀) (r : R) :
    toAddValuation v r = OrderDual.toDual (Additive.ofMul (v r)) :=
  rfl

Похожие утверждения