OAI/Combinatorics/Chromatic/Shuffle/UnitalGradeCoproductUnits.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct_zero_left line 13
2. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct_zero_right line 34
3. def OAI.ElementaryPositivity.RawShuffle.zeroGradeCounit line 64
4. lemma OAI.ElementaryPositivity.RawShuffle.zeroGradeCounit_mk line 78
5. lemma OAI.ElementaryPositivity.RawShuffle.zeroGradeCounit_one line 83
6. lemma OAI.ElementaryPositivity.RawShuffle.zeroGrade_eq_scalar line 90
7. def OAI.ElementaryPositivity.RawShuffle.globalUnit line 106
8. def OAI.ElementaryPositivity.RawShuffle.globalCounit line 110
9. lemma OAI.ElementaryPositivity.RawShuffle.globalCounit_lof_zero line 115
10. lemma OAI.ElementaryPositivity.RawShuffle.globalCounit_lof_ne line 121
11. lemma OAI.ElementaryPositivity.RawShuffle.globalCounit_unit line 127
12. lemma OAI.ElementaryPositivity.RawShuffle.globalUnit_eq_one line 131
13. lemma OAI.ElementaryPositivity.RawShuffle.globalCounit_tensor_nonzero_left line 135
14. lemma OAI.ElementaryPositivity.RawShuffle.globalCounit_tensor_nonzero_right line 148