equivWithAbs — Mathlib

English

There is a canonical ring equivalence between WithAbs v and WithAbs w for any two absolute values v and w on R.

Русский

Для любых двух абсолютных значений v и w существует каноническое эквивалентное отображение между WithAbs v и WithAbs w.

LaTeX

$$WithAbs(v) \\cong_{Ring} WithAbs(w)$$

Lean4

/-- The canonical (semiring) equivalence between `WithAbs v` and `WithAbs w`, for any two
absolute values `v` and `w` on `R`. -/
def equivWithAbs (v w : AbsoluteValue R S) : WithAbs v ≃+* WithAbs w :=
  (WithAbs.equiv v).trans <| (WithAbs.equiv w).symm

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