English
The left inversion sequence of ω is defined by: for ω = i :: ω', the sequence starts with s_i and continues by conjugating the rest by s_i.
Русский
Левая последовательность инверсий ω задаётся как: для ω = i :: ω', последовательность начинается с s_i и далее следует конъюгация остального элементами s_i.
LaTeX
$$$\text{leftInvSeq}(\omega) = \begin{cases}[] & \text{if } \omega = [],\\ s_i :: \text{map}(\text{MulAut.conj}(s_i))\big(\text{leftInvSeq}(\omega')\big) & \text{if } \omega = i :: \omega'\end{cases}$$$
Lean4
/-- The left inversion sequence of `ω`. The left inversion sequence of a word
$s_{i_1} \cdots s_{i_\ell}$ is the sequence
$$s_{i_1}, s_{i_1}s_{i_2}s_{i_1}, s_{i_1}s_{i_2}s_{i_3}s_{i_2}s_{i_1}, \ldots,
s_{i_1}\cdots s_{i_\ell}\cdots s_{i_1}.$$
-/
def leftInvSeq (ω : List B) : List W :=
match ω with
| [] => []
| i :: ω => s i :: List.map (MulAut.conj (s i)) (leftInvSeq ω)
