def CoxeterMatrix.restrictToSet {B : Type u_1} (M : CoxeterMatrix B) (T : Set B) : CoxeterMatrix ↑T

Restriction of a Coxeter matrix $M$ to a subset $T \subseteq B$, giving the Coxeter matrix of the parabolic subsystem indexed by $T$.

theorem zpow_eq_one_or_self_of_sq_eq_one {G : Type u_1} [Group G] {x : G} (h : x * x = 1) (n : ℤ) : x ^ n = 1 ∨ x ^ n = x

Group-theoretic helper: any integer power of an involution $x$ (with $x^2 = 1$) is either $1$ or $x$.

theorem CoxeterSystem.simple_ne_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.simple i ≠ 1

Each simple reflection $s_i \in W$ is nontrivial, i.e. $s_i \neq 1$.

theorem CoxeterSystem.mul_simple_ne_self {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : w ≠ w * cs.simple i

Right-multiplying by a simple generator changes the element: $w \neq w \cdot s_i$.

def CoxeterSystem.parabolicSubgroup {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (T : Set B) : Subgroup W

Parabolic subgroup $W_T \subseteq W$: the subgroup generated by the simple reflections $\{s_i : i \in T\}$.

theorem CoxeterSystem.parabolicSubgroup_mono {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {T T' : Set B} (h : T ⊆ T') : cs.parabolicSubgroup T ≤ cs.parabolicSubgroup T'

Monotonicity of parabolic subgroups: $T \subseteq T' \Rightarrow W_T \leq W_{T'}$.