toDegLex_add

Mathlib.Data.Finsupp.MonomialOrder.DegLex

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

English

The map toDegLex preserves addition: toDegLex(a + b) = toDegLex(a) + toDegLex(b) for all a, b in α.

Русский

Отображение toDegLex сохраняет сложение: toDegLex(a + b) = toDegLex(a) + toDegLex(b) для всех a, b ∈ α.

LaTeX

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

Lean4

theorem toDegLex_add [AddCommMonoid α] (a b : α) : toDegLex (a + b) = toDegLex a + toDegLex b :=
  rfl

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

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

Разделы

Аффилиация

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