OAI/Combinatorics/Chromatic/Shuffle/SlopeGridSum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElementaryPositivity.RawShuffle.SlopeColumnGrid line 12
2. def OAI.ElementaryPositivity.RawShuffle.slopeColumnEquiv line 16
3. lemma OAI.ElementaryPositivity.RawShuffle.sum_dite_zero_subtype line 48
4. lemma OAI.ElementaryPositivity.RawShuffle.sum_slope_column line 60
5. lemma OAI.ElementaryPositivity.RawShuffle.globalSplitCoproduct_eq line 90
6. lemma OAI.ElementaryPositivity.RawShuffle.globalColumnGradeTerm line 97
7. lemma OAI.ElementaryPositivity.RawShuffle.globalSplitCoproduct_shuffle line 121
8. lemma OAI.ElementaryPositivity.RawShuffle.globalCoproduct_mul_lof line 142
9. theorem OAI.ElementaryPositivity.RawShuffle.globalCoproduct_mul line 170