toValuation_apply — Mathlib

English

The value of the valuation obtained from an additive valuation v at an argument r is the multiplicative image of the dual of v(r): (toValuation v)(r) = Multiplicative.ofAdd(OrderDual.toDual(v(r))).

Русский

Значение оценки, полученной из аддитивной оценки v, на аргументе r есть образ под множителем через двойственное отображение: (toValuation v)(r) = Multiplicative.ofAdd(OrderDual.toDual(v(r))).

LaTeX

$$$$ (\mathrm{toValuation}\ v)\ r = \mathrm{Multiplicative.ofAdd}(\mathrm{OrderDual.toDual}(v(r))). $$$$

Lean4

@[simp]
theorem toValuation_apply (r : R) : toValuation v r = Multiplicative.ofAdd (OrderDual.toDual (v r)) :=
  rfl

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