ofValuation_apply — Mathlib

English

The AddValuation corresponding to a Valuation v satisfies: (ofValuation v) r = OrderDual.ofDual(Multiplicative.toAdd(v r)).

Русский

Аддитивная оценка, соответствующая оценке v, удовлетворяет: (ofValuation v) r = OrderDual.ofDual(Multiplicative.toAdd(v r)).

LaTeX

$$$$ (\mathrm{ofValuation} \, v)\ r = \mathrm{OrderDual.ofDual}(\mathrm{Multiplicative.toAdd}(v(r))). $$$$

Lean4

@[simp]
theorem ofValuation_apply (v : Valuation R (Multiplicative Γ₀ᵒᵈ)) (r : R) :
    ofValuation v r = OrderDual.ofDual (Multiplicative.toAdd (v r)) :=
  rfl

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