OAI/Combinatorics/Chromatic/Shuffle/UnitalShuffleCoproduct.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.ElementaryPositivity.RawShuffle.SlopeSplitline 15 - def
OAI.ElementaryPositivity.RawShuffle.globalTensorGradeInclusionline 18 - def
OAI.ElementaryPositivity.RawShuffle.globalSplitCoproductline 29 - def
OAI.ElementaryPositivity.RawShuffle.globalHomogeneousCoproductline 40 - def
OAI.ElementaryPositivity.RawShuffle.globalCoproductline 46 - lemma
OAI.ElementaryPositivity.RawShuffle.globalCoproduct_lofline 54