Commit 2024-05-11 18:18 0e70892c
View on Github →feat: length, reduced words in Coxeter groups (#11465)
Add new file GroupTheory/Coxeter/Length.lean
. Define the length function and reduced words of Coxeter groups. Prove their basic properties.
I decided to split #11408 (now closed) into two pull requests. This is the first one.