OAI/Combinatorics/Chromatic/Shuffle/ExtendPolynomial.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.SplitTree.extendPolynomial line 11
2. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.extendPolynomial_C line 16
3. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.extendPolynomial_X line 21
4. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.extendPolynomial_map line 26
5. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.extendPolynomial_preMap line 34
6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.toMvPolynomial_map line 42
7. def OAI.ElementaryPositivity.RawShuffle.SplitTree.Centers line 58
8. def OAI.ElementaryPositivity.RawShuffle.SplitTree.centerTranslation line 62
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerTranslation_tmul line 74
10. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerTranslation_natural line 85
11. def OAI.ElementaryPositivity.RawShuffle.SplitTree.rawCenteredRestriction line 109
12. def OAI.ElementaryPositivity.RawShuffle.SplitTree.centeredRestrictionB line 113
13. theorem OAI.ElementaryPositivity.RawShuffle.SplitTree.centeredRestrictionB_mk line 120