English
An ordered monoid isomorphism f induces an equivalence between valuations, compatible with map, map_add, and map_sub.
Русский
Упомянутый упорядоченный изоморфизм Γ0 ≃*o Γ'0 порождает эквивалентность между оценками, совместимую с отображением, сложением и вычитанием.
LaTeX
$$$\\text{congr}(f) : Valuation\\ R\\ Γ_0 \\simeq Valuation\\ R\\ Γ'_0$$$
Lean4
/-- An ordered monoid isomorphism `Γ₀ ≃ Γ'₀` induces an equivalence
`Valuation R Γ₀ ≃ Valuation R Γ'₀`. -/
def congr (f : Γ₀ ≃*o Γ'₀) : Valuation R Γ₀ ≃ Valuation R Γ'₀
where
toFun := map f f.toOrderIso.monotone
invFun := map f.symm f.toOrderIso.symm.monotone
left_inv ν := by ext; simp
right_inv ν := by ext; simp
