equiv

Mathlib.Analysis.Normed.Ring.WithAbs

URI: https://scilib.ai/kg/mathlib#WithAbs.equiv

English

There is a canonical ring equivalence between WithAbs v and R.

Русский

Существует каноническое эквивалентное отображение между WithAbs v и R как кольцами.

LaTeX

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

Lean4

/-- The canonical (semiring) equivalence between `WithAbs v` and `R`. -/
def equiv : WithAbs v ≃+* R :=
  RingEquiv.refl _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru