theorem CoxeterGroup.wordSigma_append_s_neg {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) : wordSigma M (word ++ [s]) (e s) = fun (t : B) => -wordSigma M word (e s) t

Appending $s$ at the end of a word negates the geometric action on $e_s$: $(w \cdot s) \cdot e_s = -(w \cdot e_s)$.

theorem CoxeterGroup.bilinInversions_singleton {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : bilinInversions M [s] = {s}

The inversion set of the singleton word $[s]$ is exactly $\{s\}$.