invRev — Mathlib

English

The inverse word is obtained by flipping the sign of each letter and reversing the order.

Русский

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

LaTeX

$$$\mathrm{invRev}(w) = \big(\mathrm{map}(\lambda g:(\alpha,\mathrm{Bool})\,\to\,(g.1, \neg g.2))\, w\big)\;\mathrm{reverse}.$$$

Lean4

/-- Transform a word representing a free group element into a word representing its inverse. -/
@[to_additive /-- Transform a word representing a free group element into a word representing its
      negative. -/
    ]
def invRev (w : List (α × Bool)) : List (α × Bool) :=
  (List.map (fun g : α × Bool => (g.1, not g.2)) w).reverse

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