OAI/Combinatorics/Chromatic/Shuffle/PointEvaluation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.constantCoeff_translation line 13
2. def OAI.ElementaryPositivity.RawShuffle.translationAlgB line 21
3. lemma OAI.ElementaryPositivity.RawShuffle.translationAlgB_apply line 27
4. def OAI.ElementaryPositivity.RawShuffle.SplitTree.centerOfVar line 34
5. def OAI.ElementaryPositivity.RawShuffle.SplitTree.translationAtAlgB line 39
6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.translationAtAlgB_apply line 46
7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.degreeZero_translate_quotient line 60
8. def OAI.ElementaryPositivity.RawShuffle.SplitTree.pointedRestrictionB line 84
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.pointedRestrictionB_mk line 91
10. instance OAI.ElementaryPositivity.RawShuffle.SplitTree.centersFintype line 110
11. instance OAI.ElementaryPositivity.RawShuffle.SplitTree.centersLinearOrder line 117
12. def OAI.ElementaryPositivity.RawShuffle.SplitTree.centerPairs line 124
13. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerPairs_ne line 128
14. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerPairs_norev line 132
15. def OAI.ElementaryPositivity.RawShuffle.SplitTree.centerNumerator line 137
16. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerDenominator_ne_zero line 142
17. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerNumerator_ne_zero line 148
18. def OAI.ElementaryPositivity.RawShuffle.SplitTree.PairSymmetric line 153
19. def OAI.ElementaryPositivity.RawShuffle.SplitTree.clearedLeading line 157
20. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.denominator_clearedLeading line 165
21. def OAI.ElementaryPositivity.RawShuffle.SplitTree.clearedLeadingMap line 174
22. def OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedSymbol line 191
23. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedSymbol_eq_zero_iff line 199