Exchange condition for a Coxeter group (source code)

= Exchange condition for a Coxeter group

If $w=s_1\cdots s_n$ is a reduced expression and $s$ is simple with $\ell(ws)<\ell(w)$, then
$$
ws=s_1\cdots\widehat{s_j}\cdots s_n
$$
for some index $j$. The analogous statement holds for multiplication on the left.