OAI/Combinatorics/Chromatic/Shuffle/GlobalCoproductIteration.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ElementaryPositivity.RawShuffle.globalGradeLofline 13 - def
OAI.ElementaryPositivity.RawShuffle.globalSplitGradeCoproductline 18 - lemma
OAI.ElementaryPositivity.RawShuffle.globalCoproduct_tensor_leftline 25 - lemma
OAI.ElementaryPositivity.RawShuffle.globalCoproduct_tensor_rightline 59 - def
OAI.ElementaryPositivity.RawShuffle.globalIteratedLeftSplitline 93 - def
OAI.ElementaryPositivity.RawShuffle.globalIteratedRightSplitline 108 - lemma
OAI.ElementaryPositivity.RawShuffle.globalCoproduct_iterated_left_lofline 123 - lemma
OAI.ElementaryPositivity.RawShuffle.globalCoproduct_iterated_right_lofline 139