def CoxeterGroup.IsRoot {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v : B → ℝ) : Prop

A vector $v \in \mathbb{R}^B$ is a root if $v = \sigma_w(\alpha_s)$ for some word $w$ and simple generator $s$.

def CoxeterGroup.roots {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Set (B → ℝ)

The root system $\Phi = W \cdot \{\alpha_s : s \in S\}$ of $M$.

def CoxeterGroup.positiveRoots {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Set (B → ℝ)

The positive roots $\Phi^+ \subseteq \Phi$: roots with all coordinates $\geq 0$.

def CoxeterGroup.negativeRoots {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Set (B → ℝ)

The negative roots $\Phi^- \subseteq \Phi$: roots with all coordinates $\leq 0$.

def CoxeterGroup.inversions {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (w : List B) : Set (B → ℝ)

Inversion set of a word $w$: positive roots $v$ such that $\sigma_w(v) \in \Phi^-$.

noncomputable def CoxeterGroup.generalizedReflection {B : Type u_1} [Fintype B] (M : CoxeterMatrix B) (β : B → ℝ) : (B → ℝ) → B → ℝ

Generalized reflection along a root $\beta$: $s_\beta(v) = v - 2\,B_M(v, \beta)\,\beta$.