OAI/Combinatorics/Chromatic/Shuffle/Degree.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.componentS_zero line 15
2. lemma OAI.ElementaryPositivity.RawShuffle.componentS_zero_mul line 21
3. def OAI.ElementaryPositivity.RawShuffle.degreeZeroB line 27
4. lemma OAI.ElementaryPositivity.RawShuffle.degreeZeroB_mk line 56
5. def OAI.ElementaryPositivity.RawShuffle.SplitTree.zeroDegrees line 62
6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.totalDegree_zeroDegrees line 67
7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.nonnegativeDegree_zeroDegrees line 73
8. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.nonnegative_totalDegree_zero line 79
9. def OAI.ElementaryPositivity.RawShuffle.SplitTree.degreeZeroTensor line 89
10. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.degreeZeroTensor_apply line 93
11. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.sub_degreeZero_mem line 106
12. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.translationAtB_add line 132
13. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.restrictionB_translationAt line 147
14. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centeredRestrictionB_translate_eval line 170
15. lemma OAI.ElementaryPositivity.RawShuffle.sourceFiltration_translation_mem line 182