OAI/Combinatorics/Chromatic/Shuffle/EulerForm.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.eulerForm line 13
2. lemma OAI.ElementaryPositivity.RawShuffle.diagonal_homogeneous line 16
3. lemma OAI.ElementaryPositivity.RawShuffle.cutFactor_homogeneous line 22
4. lemma OAI.ElementaryPositivity.RawShuffle.cutDenominator_homogeneous line 34
5. lemma OAI.ElementaryPositivity.RawShuffle.cutNumerator_homogeneous line 41
6. lemma OAI.ElementaryPositivity.RawShuffle.naturalVandermonde_homogeneous line 64
7. theorem OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_homogeneous line 72
8. def OAI.ElementaryPositivity.RawShuffle.componentS line 126
9. lemma OAI.ElementaryPositivity.RawShuffle.componentS_val line 134
10. lemma OAI.ElementaryPositivity.RawShuffle.componentS_homogeneous line 138
11. lemma OAI.ElementaryPositivity.RawShuffle.sum_componentS line 143
12. lemma OAI.ElementaryPositivity.RawShuffle.componentS_of_homogeneous line 151
13. lemma OAI.ElementaryPositivity.RawShuffle.componentS_dimensionCast line 161
14. lemma OAI.ElementaryPositivity.RawShuffle.homogeneous_dimensionCast line 167
15. lemma OAI.ElementaryPositivity.RawShuffle.shuffleLinear_apply line 173
16. lemma OAI.ElementaryPositivity.RawShuffle.shuffle_sum_components line 176
17. theorem OAI.ElementaryPositivity.RawShuffle.componentS_destabilizing_mem line 185