noncomputable def CoxeterGroup.bilinInversions {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) : Finset B

The bilinear inversion set of a word $w$: the set of $s \in S$ for which the $s$-component of $\sigma_w(\alpha_s)$ is strictly negative.

theorem CoxeterGroup.bilinInversions_nil {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : bilinInversions M [] = ∅

The empty word has empty inversion set.

theorem CoxeterGroup.s_in_bilinInversions_singleton {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : s ∈ bilinInversions M [s]

The singleton word $[s]$ has $s$ as an inversion.

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 \neq t$, the $t$-component of $\sigma_s(\alpha_t)$ equals $1$.

theorem CoxeterGroup.t_not_in_bilinInversions_singleton {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) : t ∉ bilinInversions M [s]

For $s \neq t$, the singleton word $[s]$ does not have $t$ as an inversion.

theorem CoxeterGroup.mem_bilinInversions_iff {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) : s ∈ bilinInversions M word ↔ wordSigma M word (e s) s < 0

Membership in the bilinear inversion set: $s \in \mathrm{Inv}(w) \iff (\sigma_w \alpha_s)_s < 0$.