reduce_toWord — Mathlib

English

For every x in the free group, reducing the word of x yields the same word: reduce (toWord x) = toWord x.

Русский

Для любого x из свободной группы редукция слова x возвращает то же самое слово: reduce (toWord x) = toWord x.

LaTeX

$$$\forall x : FreeGroup\,\alpha ,\; \mathrm{reduce}(\mathrm{toWord}(x)) = \mathrm{toWord}(x)$$$

Lean4

@[to_additive (attr := simp)]
theorem reduce_toWord : ∀ x : FreeGroup α, reduce (toWord x) = toWord x :=
  by
  rintro ⟨L⟩
  exact reduce.idem

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