instDecidableEq

Mathlib.GroupTheory.FreeGroup.Reduce

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

English

Reduction of inverse-reverse with left cancellation yields the empty word (duplicate): reduce (invRev L ++ L) = [].

Русский

Редукция invRev(L) с левой стороны от L даёт пустое слово (дубликат): reduce (invRev L ++ L) = [].

LaTeX

$$$\forall L : List(Prod\;\alpha\;Bool),\; \mathrm{reduce}(\mathrm{invRev} L ++ L) = []$$$

Lean4

@[to_additive]
instance : DecidableEq (FreeGroup α) :=
  toWord_injective.decidableEq

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

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

Разделы

Аффилиация

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