inv_def — Mathlib

English

The inverse in the coproduct of two groups is given by reversing the word and applying inverses to each letter.

Русский

Обратное в копродукте двух групп задаётся разворотом слова и применением обратных к каждой букве.

LaTeX

$$$ (\mathrm{mk} w)^{-1} = \mathrm{mk}\big(\mathrm{ofList}(w.toList.map(\mathrm{Sum.mapInvInv}).reverse)\big). $$$

Lean4

@[to_additive]
theorem inv_def (w : FreeMonoid (G ⊕ H)) : (mk w)⁻¹ = mk (ofList (w.toList.map (Sum.map Inv.inv Inv.inv)).reverse) :=
  rfl

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