instRing

Mathlib.Analysis.Normed.Ring.WithAbs

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

English

If R has a ring structure, then WithAbs v has a ring structure.

Русский

Если R имеет структуру кольца, то WithAbs v имеет структуру кольца.

LaTeX

$$Ring(WithAbs(v))$$

Lean4

instance instRing [Ring R] (v : AbsoluteValue R S) : Ring (WithAbs v) :=
  inferInstanceAs (Ring R)

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

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

Разделы

Аффилиация

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