theorem CoxeterGroup.wordSigma_eq_of_wordProd_eq {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) {W : Type u_2} [Group W] (cs : CoxeterSystem M W) (word1 word2 : List B) (h : cs.wordProd word1 = cs.wordProd word2) (v : B → ℝ) : wordSigma M word1 v = wordSigma M word2 v

The geometric action $\mathrm{wordSigma}$ depends only on the group element, not the word: if $\mathrm{wordProd}(w_1) = \mathrm{wordProd}(w_2)$ then $w_1 \cdot v = w_2 \cdot v$.