ofDegLex_add

Mathlib.Data.Finsupp.MonomialOrder.DegLex

URI: https://scilib.ai/kg/mathlib#ofDegLex_add

English

The map ofDegLex preserves addition on DegLex objects: ofDegLex(a + b) = ofDegLex(a) + ofDegLex(b).

Русский

Отображение ofDegLex сохраняет сложение: ofDegLex(a + b) = ofDegLex(a) + ofDegLex(b) для DegLex α

LaTeX

$$$\operatorname{ofDegLex}(a + b) = \operatorname{ofDegLex}(a) + \operatorname{ofDegLex}(b)$$$

Lean4

theorem ofDegLex_add [AddCommMonoid α] (a b : DegLex α) : ofDegLex (a + b) = ofDegLex a + ofDegLex b :=
  rfl

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

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

Разделы

Аффилиация

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