toWord_inv — Mathlib

English

The word of the inverse in the free group is the inverse-reverse of the word: toWord(x^{-1}) = invRev(toWord x).

Русский

Слово обратного элемента в свободной группе равно развёрнутому слову: toWord(x^{-1}) = invRev(toWord x).

LaTeX

$$$\forall x : FreeGroup\,\alpha ,\; x^{-1}.toWord = invRev(x.toWord)$$$

Lean4

@[to_additive (attr := simp)]
theorem toWord_inv (x : FreeGroup α) : x⁻¹.toWord = invRev x.toWord :=
  by
  rcases x with ⟨L⟩
  rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]

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