OAI/Combinatorics/Chromatic/Shuffle/UnitalGrade.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.UnitalSourceGrade line 14
2. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 17) line 17
3. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 20) line 20
4. def OAI.ElementaryPositivity.RawShuffle.UnitalSourceTensorGrade line 24
5. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 28) line 28
6. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 31) line 31
7. def OAI.ElementaryPositivity.RawShuffle.unitalGradeShuffle line 35
8. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeShuffle_mk line 54
9. def OAI.ElementaryPositivity.RawShuffle.unitalSeparationConstant line 64
10. def OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct line 71
11. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct_mk line 82
12. def OAI.ElementaryPositivity.RawShuffle.unitalSourceTensorGradeEquiv line 90