OAI/Combinatorics/Chromatic/Shuffle/GlobalWordDetection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.signedWordCuts_perm line 17
2. lemma OAI.ElementaryPositivity.RawShuffle.singletonCutSum_not_mem line 29
3. lemma OAI.ElementaryPositivity.RawShuffle.singletonCutSum_congr line 41
4. lemma OAI.ElementaryPositivity.RawShuffle.singletonCutSum_unique line 54
5. lemma OAI.ElementaryPositivity.RawShuffle.functionalWord_top_not_perm line 58
6. lemma OAI.ElementaryPositivity.RawShuffle.singletonCutSum_even_sorted line 91
7. lemma OAI.ElementaryPositivity.RawShuffle.functionalWord_top_sorted_ne line 114
8. def OAI.ElementaryPositivity.RawShuffle.PBWAdmissible line 140
9. lemma OAI.ElementaryPositivity.RawShuffle.PBWAdmissible.sorted line 144
10. lemma OAI.ElementaryPositivity.RawShuffle.PBWAdmissible.tail line 148
11. lemma OAI.ElementaryPositivity.RawShuffle.singletonCutSum_sorted_self line 153
12. def OAI.ElementaryPositivity.RawShuffle.wordMultiplicity line 175
13. lemma OAI.ElementaryPositivity.RawShuffle.wordMultiplicity_pos line 180
14. lemma OAI.ElementaryPositivity.RawShuffle.functionalWord_diagonal line 185