Commit 2024-05-23 01:17 4072ed93

feat: reflections, inversion sequences in Coxeter groups (#11466)

• Add theorem List.length_eraseIdx_add_one to Data/List/Basic.lean, which states that if i < l.length, then the length of l.eraseIdx i plus one is equal to the length of l.
• Add new file GroupTheory/Coxeter/Inversion.lean. Define reflections, left inversions, right inversions, and inversion sequences. Prove their basic properties. I decided to split #11408 (now closed) into two pull requests. This is the second one. The first is #11465.