English
For a family of groups, the inverse of a NeWord is obtained by reversing the order of its components and inverting each letter, yielding inv(w) : NeWord G j i for w : NeWord G i j.
Русский
Для группы инверсия NeWord строится как обращение порядка компонент и взятие каждого элемента в обратном виде: inv(w) : NeWord G j i, если w : NeWord G i j.
LaTeX
$$$$\\text{inv} : \\mathrm{NeWord}\\ G\\ i\\ j \\to \\mathrm{NeWord}\\ G\\ j\\ i.$$$$
Lean4
/-- The inverse of a non-empty reduced word -/
def inv : ∀ {i j} (_w : NeWord G i j), NeWord G j i
| _, _, singleton x h => singleton x⁻¹ (mt inv_eq_one.mp h)
| _, _, append w₁ h w₂ => append w₂.inv h.symm w₁.inv
