OAI/Combinatorics/Chromatic/Shuffle/UnitalGradeAlgebra.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.slopeZero line 12
2. lemma OAI.ElementaryPositivity.RawShuffle.shuffleBUnit_assoc line 14
3. def OAI.ElementaryPositivity.RawShuffle.unitalFiltrationCast line 34
4. def OAI.ElementaryPositivity.RawShuffle.unitalGradeCast line 41
5. lemma OAI.ElementaryPositivity.RawShuffle.unitalFiltrationCast_val line 48
6. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCast_mk line 56
7. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeShuffle_assoc line 66
8. def OAI.ElementaryPositivity.RawShuffle.unitalGradeOne line 88
9. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeShuffle_one_left line 92
10. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeShuffle_one_right line 105
11. abbrev OAI.ElementaryPositivity.RawShuffle.slopeDimensions line 126
12. abbrev OAI.ElementaryPositivity.RawShuffle.SlopeWeight line 131
13. abbrev OAI.ElementaryPositivity.RawShuffle.unitalComponent line 134
14. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCast_heq line 138
15. instance OAI.ElementaryPositivity.RawShuffle.componentGradedMul line 146
16. instance OAI.ElementaryPositivity.RawShuffle.componentGradedOne line 151
17. lemma OAI.ElementaryPositivity.RawShuffle.component_one_mul line 155
18. lemma OAI.ElementaryPositivity.RawShuffle.component_mul_one line 162
19. lemma OAI.ElementaryPositivity.RawShuffle.component_mul_assoc line 169
20. instance OAI.ElementaryPositivity.RawShuffle.componentGradedMonoid line 178
21. instance OAI.ElementaryPositivity.RawShuffle.componentGradedRing line 184
22. lemma OAI.ElementaryPositivity.RawShuffle.component_smul_mul line 201
23. lemma OAI.ElementaryPositivity.RawShuffle.component_mul_smul line 211
24. instance OAI.ElementaryPositivity.RawShuffle.componentGradedAlgebra line 219
25. abbrev OAI.ElementaryPositivity.RawShuffle.UnitalShuffle line 224