instUniqueAddUnits

Mathlib.Combinatorics.Enumerative.DyckWord

URI: https://scilib.ai/kg/mathlib#DyckWord.instUniqueAddUnits

Lean4

/-- The only Dyck word that is an additive unit is the empty word. -/
instance : Unique (AddUnits DyckWord) where
  uniq
    p := by
    obtain ⟨a, b, h, -⟩ := p
    obtain ⟨ha, hb⟩ := append_eq_nil_iff.mp (toList_eq_nil.mpr h)
    congr
    · exact toList_eq_nil.mp ha
    · exact toList_eq_nil.mp hb

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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