toWord_of

Mathlib.GroupTheory.FreeGroup.Reduce

URI: https://scilib.ai/kg/mathlib#FreeGroup.toWord_of

English

The word of a single generator a is the singleton word [(a, true)].

Русский

Слово генератора a есть односоставное слово [(a, true)].

LaTeX

$$$\mathrm{toWord}(\mathrm{of}(a)) = [(a, true)]$$$

Lean4

@[to_additive (attr := simp)]
theorem toWord_of (a : α) : (of a).toWord = [(a, true)] :=
  rfl

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

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

Разделы

Аффилиация

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