OAI/Combinatorics/Chromatic/Shuffle/Split.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.ShuffleConvolution.Split line 9
2. instance OAI.ElementaryPositivity.ShuffleConvolution.(instance at line 10) line 10
3. instance OAI.ElementaryPositivity.ShuffleConvolution.(instance at line 11) line 11
4. lemma OAI.ElementaryPositivity.ShuffleConvolution.Split.left_subset line 14
5. lemma OAI.ElementaryPositivity.ShuffleConvolution.Split.right_subset line 19
6. abbrev OAI.ElementaryPositivity.ShuffleConvolution.LeftIndex line 24
7. abbrev OAI.ElementaryPositivity.ShuffleConvolution.RightIndex line 25
8. def OAI.ElementaryPositivity.ShuffleConvolution.rebracket line 27
9. def OAI.ElementaryPositivity.ShuffleConvolution.kernel line 61
10. lemma OAI.ElementaryPositivity.ShuffleConvolution.kernel_union_left line 64
11. lemma OAI.ElementaryPositivity.ShuffleConvolution.kernel_union_right line 69
12. lemma OAI.ElementaryPositivity.ShuffleConvolution.kernel_cocycle line 74
13. def OAI.ElementaryPositivity.ShuffleConvolution.shuffle line 81
14. lemma OAI.ElementaryPositivity.ShuffleConvolution.shuffle_assoc line 84
15. lemma OAI.ElementaryPositivity.ShuffleConvolution.shuffle_add_left line 112
16. lemma OAI.ElementaryPositivity.ShuffleConvolution.shuffle_add_right line 116
17. lemma OAI.ElementaryPositivity.ShuffleConvolution.shuffle_supported_degree line 121