OAI/Combinatorics/Chromatic/Shuffle/RestrictionTestHomogeneity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.restrictionTest_homogeneous line 16
2. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.restrictionTest_component line 85
3. lemma OAI.ElementaryPositivity.RawShuffle.sourceFiltration_component_mem line 107
4. def OAI.ElementaryPositivity.RawShuffle.derivativeS line 125
5. lemma OAI.ElementaryPositivity.RawShuffle.derivativeS_val line 129
6. def OAI.ElementaryPositivity.RawShuffle.derivativeB line 135
7. lemma OAI.ElementaryPositivity.RawShuffle.derivativeB_mk line 139
8. lemma OAI.ElementaryPositivity.RawShuffle.derivativeS_pow_val line 146
9. lemma OAI.ElementaryPositivity.RawShuffle.derivativeB_pow_mk line 154
10. theorem OAI.ElementaryPositivity.RawShuffle.derivativeB_locally_nilpotent line 161
11. lemma OAI.ElementaryPositivity.RawShuffle.derivativeB_mul line 174
12. lemma OAI.ElementaryPositivity.RawShuffle.derivativeB_filtered line 181
13. def OAI.ElementaryPositivity.RawShuffle.gradeDerivative line 190