ofAddValuation — Mathlib

English

There is a canonical involutive correspondence between AddValuation and Valuation, so that the inverse of the canonical map is the forward map.

Русский

Существует каноническое взаимно-однозначное соответствие между AddValuation и Valuation, поэтому обратное отображение эквивариантно прямому.

LaTeX

$$$ (\\text{toAddValuation})^{-1} = \\text{ofAddValuation}. $$$

Lean4

/-- The `Valuation` associated to a `AddValuation`.
-/
def ofAddValuation : AddValuation R (Additive Γ₀)ᵒᵈ ≃ Valuation R Γ₀ :=
  AddValuation.toValuation.trans <|
    congr <|
      { toFun := fun x ↦ x.toAdd.ofDual.ofDual.toMul
        invFun := fun x ↦ .ofAdd <| .toDual <| .toDual <| .ofMul x
        map_mul' := fun _x _y ↦ rfl
        map_le_map_iff' := .rfl }

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