noncomputable def CoxeterGroup.sigmaWord {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : List B → Module.End ℝ (B → ℝ)

The endomorphism of $\mathbb{R}^B$ associated to a word $s_1 \cdots s_k$, defined as the product $\sigma_{s_1} \circ \cdots \circ \sigma_{s_k}$ in $\mathrm{End}_{\mathbb{R}}(\mathbb{R}^B)$.

@[simp]

theorem CoxeterGroup.sigmaWord_cons {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (w : List B) : sigmaWord M (s :: w) = sigmaLin M s * sigmaWord M w

Cons unfolding of sigmaWord.

theorem CoxeterGroup.sigmaWord_singleton {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : sigmaWord M [s] = sigmaLin M s

Singleton: sigmaWord M [s] = sigmaLin M s.