English
There is a canonical equivalence between valuations on R with Γ0 and AddValuations on R with Additive Γ0 in the opposite order.
Русский
Существует каноническое эквивалентное взаимно однозначное соответствие между валюациями R с γ и AddValuations R с Additive γ, взятое в противоположном порядке.
LaTeX
$$$ \\mathrm{Valuation}(R, \\Gamma_0) \\simeq \\mathrm{AddValuation}(R, \\mathrm{Additive}(\\Gamma_0))^{\\mathrm{op}}. $$$
Lean4
/-- The `AddValuation` associated to a `Valuation`. -/
def toAddValuation : Valuation R Γ₀ ≃ AddValuation R (Additive Γ₀)ᵒᵈ :=
.trans
(congr
{ toFun := fun x ↦ .ofAdd <| .toDual <| .toDual <| .ofMul x
invFun := fun x ↦ x.toAdd.ofDual.ofDual.toMul
map_mul' := fun _x _y ↦ rfl
map_le_map_iff' := .rfl })
(AddValuation.ofValuation (R := R) (Γ₀ := (Additive Γ₀)ᵒᵈ))
