mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard
verified publisher icon leanprover-community

feat: add length, reduced words in Coxeter groups

Open trivial1711 opened this issue 2 years ago • 1 comments

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.

  • [ ] depends on: #11406

Open in Gitpod

trivial1711 avatar Mar 18 '24 02:03 trivial1711

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#11406~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar Apr 26 '24 10:04 leanprover-community-mathlib4-bot