English
There is a canonical equivalence between additive valuations on R with values in Γ0 and valuations on R with values in the opposite multiplicative structure of Γ0, given by the function toValuation.
Русский
Существуют канонические эквивалентности между аддитивными оценками на R со значениями в Γ0 и оценками на R со значениями в противоположной мультипликативной структуре Γ0, задаваемые функцией toValuation.
LaTeX
$$$$ \mathrm{toValuation} : \mathrm{AddValuation}\,R\,\Gamma_0 \simeq \mathrm{Valuation}\,R\,\bigl(\mathrm{Multiplicative}(\Gamma_0^{\mathrm{op}})\bigr). $$$$
Lean4
/-- The `Valuation` associated to an `AddValuation` (useful if the latter is constructed using
`AddValuation.of`). -/
def toValuation : AddValuation R Γ₀ ≃ Valuation R (Multiplicative Γ₀ᵒᵈ) :=
Equiv.refl _
