@[reducible, inline]

noncomputable abbrev CoxeterWords.CoxGroup {B : Type u_1} (M : CoxeterMatrix B) : Type u_1

Convenience abbreviation for the Coxeter group associated to a Coxeter matrix $M$.

@[reducible, inline]

noncomputable abbrev CoxeterWords.coxeterSystem {B : Type u_1} (M : CoxeterMatrix B) : CoxeterSystem M M.Group

Convenience abbreviation for the canonical Coxeter system on M.Group.

@[reducible, inline]

noncomputable abbrev CoxeterWords.gen {B : Type u_1} (M : CoxeterMatrix B) (i : B) : M.Group

The $i$-th simple Coxeter generator $s_i$ of the Coxeter group.

@[reducible, inline]

noncomputable abbrev CoxeterWords.wordProd {B : Type u_1} (M : CoxeterMatrix B) (w : List B) : M.Group

The product $s_{i_1} \cdots s_{i_k}$ of the simple generators specified by the word $w$.

@[reducible, inline]

noncomputable abbrev CoxeterWords.wordLength {B : Type u_1} (M : CoxeterMatrix B) (w : M.Group) : ℕ

The Coxeter length $\ell(w)$ of a group element.