self — Mathlib

English

A word and its maximal reduction represent the same element in the free group: mk(reduce L) = mk(L).

Русский

Слово и его максимальное редуцирование представляют один и тот же элемент свободной группы: mk(reduce L) = mk(L).

LaTeX

$$$$\operatorname{mk}(\operatorname{reduce}(L)) = \operatorname{mk}(L).$$$$

Lean4

/-- A word and its maximal reduction correspond to the same element of the free group. -/
@[to_additive /-- A word and its maximal reduction correspond to the same element of the additive
      free group. -/
    ]
theorem self : mk (reduce L) = mk L :=
  reduce.exact reduce.idem

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