OAI/Combinatorics/Chromatic/Shuffle/GlobalCoproductUnits.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.slopeSplitZeroLeft line 14
2. def OAI.ElementaryPositivity.RawShuffle.slopeSplitZeroRight line 21
3. lemma OAI.ElementaryPositivity.RawShuffle.slopeSplit_ne_left_zero line 30
4. lemma OAI.ElementaryPositivity.RawShuffle.slopeSplit_ne_right_zero line 37
5. lemma OAI.ElementaryPositivity.RawShuffle.globalLof_gradeOne_cast line 47
6. lemma OAI.ElementaryPositivity.RawShuffle.globalSplitCoproduct_zero_left line 55
7. lemma OAI.ElementaryPositivity.RawShuffle.globalSplitCoproduct_zero_right line 67
8. lemma OAI.ElementaryPositivity.RawShuffle.globalCoproduct_counit_left_lof line 79
9. lemma OAI.ElementaryPositivity.RawShuffle.globalCoproduct_counit_right_lof line 93
10. lemma OAI.ElementaryPositivity.RawShuffle.globalCoproduct_counit_left line 107
11. lemma OAI.ElementaryPositivity.RawShuffle.globalCoproduct_counit_right line 116
12. lemma OAI.ElementaryPositivity.RawShuffle.globalCoproduct_unit line 125