OAI/Combinatorics/Chromatic/Shuffle/GlobalCoproductCocommutative.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCast_trans line 13
2. def OAI.ElementaryPositivity.RawShuffle.DimensionSplit.swap line 24
3. lemma OAI.ElementaryPositivity.RawShuffle.DimensionSplit.left_swap line 27
4. lemma OAI.ElementaryPositivity.RawShuffle.DimensionSplit.right_swap line 30
5. lemma OAI.ElementaryPositivity.RawShuffle.DimensionSplit.swap_swap line 33
6. def OAI.ElementaryPositivity.RawShuffle.slopeSplitSwap line 38
7. def OAI.ElementaryPositivity.RawShuffle.globalSignedComm line 45
8. lemma OAI.ElementaryPositivity.RawShuffle.globalSignOperator_inclusion line 51
9. lemma OAI.ElementaryPositivity.RawShuffle.globalPairCoproduct_swap line 61
10. lemma OAI.ElementaryPositivity.RawShuffle.globalSplitCoproduct_dimensions line 79
11. lemma OAI.ElementaryPositivity.RawShuffle.globalSplitCoproduct_swap line 92
12. theorem OAI.ElementaryPositivity.RawShuffle.globalCoproduct_cocommutative line 107