mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: reflections, inversion sequences in Coxeter groups

Open trivial1711 opened this issue 1 year ago • 5 comments
trafficstars

  • 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.

  • [x] depends on: #11465

Open in Gitpod

trivial1711 avatar Mar 18 '24 02:03 trivial1711