OAI/Combinatorics/Chromatic/Shuffle/SymbolSwap.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.SplitTree.centerPower line 12
2. def OAI.ElementaryPositivity.RawShuffle.SplitTree.crossPower line 16
3. def OAI.ElementaryPositivity.RawShuffle.SplitTree.crossSign line 21
4. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerPower_node line 25
5. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.crossPower_swap line 34
6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerPower_swap line 57
7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.crossSign_sq line 67
8. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.sum_leaf_euler_left line 74
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.sum_leaf_euler_right line 87
10. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.negOne_pos_neg line 99
11. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.prod_negOne line 108
12. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.crossSign_pos_neg line 117
13. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.clearedLeading_swap line 126
14. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.normalizedSymbol_swap line 163