theorem TitsExchangeFromFoldings.wordProduct_eq_mul_wordProd {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (w : M.Group) (word : List B) : TitsTheoremProof.wordProduct M w word = w * M.toCoxeterSystem.wordProd word

The typed word product accumulator equals left multiplication by the Coxeter system word product.

theorem TitsExchangeFromFoldings.wordProduct_one_eq_wordProd {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) : TitsTheoremProof.wordProduct M 1 word = M.toCoxeterSystem.wordProd word

Specialization of wordProduct_eq_mul_wordProd at $w = 1$.

theorem TitsExchangeFromFoldings.typed_gallery_deletion {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (hlong : word.length > M.toCoxeterSystem.length (M.toCoxeterSystem.wordProd word)) : ∃ (i : Fin word.length) (j : Fin word.length), i < j ∧ M.toCoxeterSystem.wordProd ((word.eraseIdx ↑j).eraseIdx ↑i) = M.toCoxeterSystem.wordProd word

Deletion condition: if a word $s_1 \dots s_n$ is longer than the length of the element it represents, then two letters can be deleted without changing the represented Coxeter element.

theorem TitsExchangeFromFoldings.exchange_condition {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : CoxeterExchange.SatisfiesExchangeCondition M M.toCoxeterSystem

The exchange condition holds unconditionally for any Coxeter system arising from a Coxeter matrix.