We formalize in Lean some results on Coxeter groups, following the textbooks [1] and [2]. The results are organized as follows:
- Basic.lean
- Basic definitions and lemmas
- Opposite.lean
- The opposite of a Coxeter group
- PermutationRepresentation.lean
- Construction of the permutation repersentation
- StrongExchange.lean
- Strong exchange
- Deletion property
- Bruhat.lean
- Definition of the Bruhat order
- Subword property
- Lifting property
- The longest element of a finite Coxeter group
[1]: A. Björner and F. Brenti, Combinatorics of Coxeter Groups. Springer, 2005. DOI: 10.1007/3-540-27596-7
[2]: N. Bourbaki, Groupes et algèbres de Lie. Springer, 2007. DOI: 10.1007/978-3-540-34491-9
