OAI/Combinatorics/Chromatic/Walls/TensorGradeFunctor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElementaryPositivity.LinearFiltration.FGrade line 16
2. def OAI.ElementaryPositivity.LinearFiltration.gradeMap line 18
3. lemma OAI.ElementaryPositivity.LinearFiltration.gradeMap_mk line 23
4. lemma OAI.ElementaryPositivity.LinearFiltration.gradeMap_id line 27
5. def OAI.ElementaryPositivity.LinearFiltration.tensorGradeMap line 35
6. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeMap_part line 43
7. def OAI.ElementaryPositivity.LinearFiltration.tensorGradeLift line 56
8. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeLift_part line 63
9. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeLift_map_natural line 72
10. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeLift_comp line 87
11. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeLift_mk_tmul line 110
12. def OAI.ElementaryPositivity.LinearFiltration.tensorGradeAssoc line 121
13. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeAssoc_mk line 129
14. lemma OAI.ElementaryPositivity.LinearFiltration.tensorGradeLift_assoc line 135