of

Mathlib.Algebra.PresentedMonoid.Basic

URI: https://scilib.ai/kg/mathlib#PresentedMonoid.of

Lean4

/-- `of` is the canonical map from `α` to a presented monoid with generators `x : α`. The term `x`
is mapped to the equivalence class of the image of `x` in `FreeMonoid α`. -/
@[to_additive /-- `of` is the canonical map from `α` to a presented additive monoid with generators `x : α`. The
    term `x` is mapped to the equivalence class of the image of `x` in `FreeAddMonoid α`. -/
    ]
def of (rels : FreeMonoid α → FreeMonoid α → Prop) (x : α) : PresentedMonoid rels :=
  mk rels (.of x)

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

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

Разделы

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

Аффилиация

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