toDegLex

Mathlib.Data.Finsupp.MonomialOrder.DegLex

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

English

The mapping toDegLex : α ≃ DegLex α is the identity equivalence on α.

Русский

Отображение toDegLex : α ≃ DegLex α есть тождественное биекция между α и DegLex α.

LaTeX

$$$\\text{toDegLex} : \\alpha \\simeq DegLex \\alpha \\quad \\text{is the identity equivalence}$$$

Lean4

/-- `toDegLex` is the identity function to the `DegLex` of a type. -/
@[match_pattern]
def toDegLex : α ≃ DegLex α :=
  Equiv.refl _

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

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

Разделы

Аффилиация

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