ofDegLex_toDegLex

Mathlib.Data.Finsupp.MonomialOrder.DegLex

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

English

For every a in α, applying toDegLex after ofDegLex returns the original element: ofDegLex(toDegLex(a)) = a.

Русский

Для любого a из α применение toDegLex после ofDegLex возвращает исходный элемент: ofDegLex(toDegLex(a)) = a.

LaTeX

$$$\operatorname{ofDegLex}(\operatorname{toDegLex}(a)) = a$$$

Lean4

@[simp]
theorem ofDegLex_toDegLex (a : α) : ofDegLex (toDegLex a) = a :=
  rfl

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

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

Разделы

Аффилиация

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