theorem CoxeterGroup.neg_e_eq_neg_one_smul_e {B : Type u_1} [DecidableEq B] (s : B) : (fun (t : B) => -e s t) = -1 • e s

Rewrites the pointwise negation of $\alpha_s$ as scalar multiplication by $-1$.

theorem CoxeterGroup.wordSigma_append_s_component_neg {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) : wordSigma M (word ++ [s]) (e s) s = -wordSigma M word (e s) s

The $s$-component of $\sigma_{w \cdot s}(\alpha_s)$ flips sign under appending $s$: $(w s)\cdot \alpha_s$ has $s$-component $-(w \cdot \alpha_s)_s$.

theorem CoxeterGroup.bilinInversions_append_toggle {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) (hne : wordSigma M word (e s) s ≠ 0) : s ∈ bilinInversions M (word ++ [s]) ↔ s ∉ bilinInversions M word

Right-multiplication by $s$ toggles whether $s$ lies in the bilinear-inversion set: $s \in \mathrm{Inv}(w s) \iff s \notin \mathrm{Inv}(w)$, provided the $s$-component is nonzero.