instCommSemiring

Mathlib.Analysis.Normed.Ring.WithAbs

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

English

If R is a commutative semiring, then WithAbs v is a commutative semiring.

Русский

Если R является коммутативным полускольцом, то WithAbs v также является коммутативным полусольцом.

LaTeX

$$WithAbs(v) \\text{ is a CommSemiring}$$

Lean4

instance instCommSemiring [CommSemiring R] (v : AbsoluteValue R S) : CommSemiring (WithAbs v) :=
  inferInstanceAs (CommSemiring R)

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

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

Разделы

Аффилиация

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