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

A vector $\alpha$ is a root iff it lies in the $W$-orbit of some simple root $e_s$, i.e. there is a word $w$ and simple $s$ with $\alpha = w \cdot e_s$.

theorem CoxeterGroup.sigma_maps_roots {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (α : B → ℝ) (hα : isRoot M α) : isRoot M (sigma M s α)

Simple reflections $\sigma_s$ map roots to roots: the root system is $W$-stable.

def CoxeterGroup.isPositiveVec {B : Type u_1} (v : B → ℝ) : Prop

A vector is strictly positive at some coordinate: $\exists s,\, v(s) > 0$.

def CoxeterGroup.isNegativeVec {B : Type u_1} (v : B → ℝ) : Prop

A vector is strictly negative at some coordinate: $\exists s,\, v(s) < 0$.

theorem CoxeterGroup.neg_e_isNegative {B : Type u_1} [DecidableEq B] [Fintype B] (s : B) : isNegativeVec fun (t : B) => -e s t

The vector $-e_s$ is strictly negative at coordinate $s$.

theorem CoxeterGroup.sigma_e_other_t_component {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) : sigma M s (e t) t = 1

For $s \ne t$, the $t$-coordinate of $\sigma_s(e_t)$ equals $1$.

def CoxeterGroup.simpleInversions {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) : Set B

The set of simple generators $s$ such that the $s$-coordinate of $w \cdot e_s$ is strictly negative — the simple inversions of the word.

noncomputable def CoxeterGroup.wordSigmaLinearMap {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) : (B → ℝ) →ₗ[ℝ] B → ℝ

The action of the word $w$ on $\mathbb{R}^B$ packaged as an $\mathbb{R}$-linear map.

theorem CoxeterGroup.wordSigma_reverse_cancel {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (v : B → ℝ) : wordSigma M word (wordSigma M word.reverse v) = v

Reversing a word inverts its geometric action: $w \cdot (w^{-1} \cdot v) = v$.