ofValuation — Mathlib

English

There is a canonical inverse correspondence from a Valuation on R to an AddValuation on R, given by AddValuation.ofValuation.

Русский

Существует каноническое обратное соответствие от оценки Valuation на R к аддитивной оценке AddValuation на R, задаваемое AddValuation.ofValuation.

LaTeX

$$$$ \mathrm{ofValuation} : \mathrm{Valuation}\,R\,\bigl(\mathrm{Multiplicative}(\Gamma_0^{\mathrm{op}})\bigr) \simeq \mathrm{AddValuation}\,R\,\Gamma_0. $$$$

Lean4

/-- The `AddValuation` associated to a `Valuation`.
-/
def ofValuation : Valuation R (Multiplicative Γ₀ᵒᵈ) ≃ AddValuation R Γ₀ :=
  Equiv.refl _

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