OAI/Combinatorics/Chromatic/Shuffle/ManyBlockPolynomiality.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.SplitTree.centerDenominator line 14
2. theorem OAI.ElementaryPositivity.RawShuffle.SplitTree.leadingPolynomial_denominator_divisible line 19
3. def OAI.ElementaryPositivity.RawShuffle.SplitTree.componentFinsupp line 54
4. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.componentFinsupp_apply line 72
5. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.componentTensor_sum line 76
6. def OAI.ElementaryPositivity.RawShuffle.SplitTree.weightComponent line 99
7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.weightComponent_eq_sum line 107
8. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.componentTensor_weightComponent line 124
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.polynomial_component_finite line 145
10. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.mapLinear_weightComponent_eq_sum line 160
11. def OAI.ElementaryPositivity.RawShuffle.SplitTree.totalLeadingPolynomial line 174
12. theorem OAI.ElementaryPositivity.RawShuffle.SplitTree.totalLeadingPolynomial_denominator_divisible line 180