uniqueUnits

Mathlib.Algebra.FreeMonoid.Basic

URI: https://scilib.ai/kg/mathlib#FreeMonoid.uniqueUnits

Lean4

/-- The only invertible element of the free monoid is 1; this instance enables `units_eq_one`. -/
@[to_additive]
instance uniqueUnits : Unique (FreeMonoid α)ˣ where
  uniq
    u :=
    Units.ext <|
      toList.injective <|
        have : toList u.val ++ toList u.inv = [] := DFunLike.congr_arg toList u.val_inv
        (List.append_eq_nil_iff.mp this).1

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

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

Разделы

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

Аффилиация

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