Coxeter Groups
February 7, 2024
Coxeter groups hold a special place in my heart, their intricate ties within mathematics and physics never failing to captivate me. I wholeheartedly encourage anyone unfamiliar with them to explore their depths and discover the inherent beauty they possess.
Embarking on this project marked a significant leap in complexity compared to anything I had previously tackled. Integrating numerous pull requests into mathlib to leverage essential results for my branch was no small feat. Additionally, honing in on the precise definitions required considerable time and effort. I extend my sincerest thanks to all the reviewers and Zulip users who generously offered their assistance and expertise.
Instead of presenting the source code here, which risks becoming outdated, I invite you to explore the most current and up-to-date version within the mathlib repository here.