theorem CoxeterGroup.rotation_power_e_s {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : (fun (w : B → ℝ) => sigma M s (sigma M t w))^[M.M s t] (e s) = e s

The braid relation for $e_s$: $(\sigma_s\sigma_t)^{m(s,t)} (e_s) = e_s$.

theorem CoxeterGroup.rotation_power_e_t {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : (fun (w : B → ℝ) => sigma M s (sigma M t w))^[M.M s t] (e t) = e t

The braid relation for $e_t$: $(\sigma_s\sigma_t)^{m(s,t)} (e_t) = e_t$.

theorem CoxeterGroup.formVal_sq_lt_one {B : Type u_1} (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : formVal M s t ^ 2 < 1

For $s \ne t$ and finite $m(s,t)$, the matrix entry satisfies $B_{s,t}^2 < 1$.

theorem CoxeterGroup.one_sub_formVal_sq_ne_zero {B : Type u_1} (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : 1 - formVal M s t ^ 2 ≠ 0

$1 - B_{s,t}^2 \ne 0$, so the orthogonal projection used below is well-defined.

noncomputable def CoxeterGroup.decompAlpha {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (v : B → ℝ) : ℝ

The coefficient $\alpha$ in the decomposition $v = \alpha e_s + \beta e_t + w$ where $w$ is $B$-orthogonal to both $e_s$ and $e_t$.

noncomputable def CoxeterGroup.decompBeta {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (v : B → ℝ) : ℝ

The coefficient $\beta$ in the orthogonal decomposition of $v$ along $e_s, e_t$, complementary to $\alpha$.

noncomputable def CoxeterGroup.decompW {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (v : B → ℝ) : B → ℝ

The orthogonal complement $w = v - \alpha e_s - \beta e_t$ of $v$ in the $(e_s, e_t)$-plane.

theorem CoxeterGroup.decomp_eq {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (v : B → ℝ) : v = decompAlpha M s t v • e s + decompBeta M s t v • e t + decompW M s t v

The decomposition identity: $v = \alpha e_s + \beta e_t + w$.

theorem CoxeterGroup.decomp_ortho_s {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (v : B → ℝ) (hst : s ≠ t) (hm : M.M s t ≠ 0) : bilinForm M (decompW M s t v) (e s) = 0

The component $w$ is $B$-orthogonal to $e_s$.

theorem CoxeterGroup.decomp_ortho_t {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (v : B → ℝ) (hst : s ≠ t) (hm : M.M s t ≠ 0) : bilinForm M (decompW M s t v) (e t) = 0

The component $w$ is $B$-orthogonal to $e_t$.

theorem CoxeterGroup.braid_power_ne {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) (v : B → ℝ) : (fun (w : B → ℝ) => sigma M s (sigma M t w))^[M.M s t] v = v

For $s \ne t$ with finite Coxeter order $m(s,t)$, the geometric representation satisfies the braid relation $(\sigma_s \sigma_t)^{m(s,t)} v = v$ on every vector $v$.

noncomputable def CoxeterGroup.braidRelationHyp {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : BraidRelationHyp M

The braid relation hypothesis holds on the geometric representation: for every pair $s, t$ with finite Coxeter order, $(\sigma_s\sigma_t)^{m(s,t)}$ is the identity on $\mathbb{R}^B$.