OAI/Combinatorics/Chromatic/Shuffle/HNZeroRows.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.slopeValue_eq_zero_iff line 19
2. lemma OAI.ElementaryPositivity.RawShuffle.decorated_zero_each line 23
3. lemma OAI.ElementaryPositivity.RawShuffle.lowIndex_singleton line 42
4. def OAI.ElementaryPositivity.RawShuffle.lowFromRow line 75
5. lemma OAI.ElementaryPositivity.RawShuffle.lowFromRow_injective line 79
6. def OAI.ElementaryPositivity.RawShuffle.lowRowsEquiv line 85
7. lemma OAI.ElementaryPositivity.RawShuffle.lowFromRow_energy line 93
8. lemma OAI.ElementaryPositivity.RawShuffle.blockRowsEnergy_admissible line 98
9. lemma OAI.ElementaryPositivity.RawShuffle.lowSeries_on_slope line 105
10. abbrev OAI.ElementaryPositivity.RawShuffle.PrimitiveCounts line 126
11. def OAI.ElementaryPositivity.RawShuffle.primitiveCountsEnergy line 130
12. lemma OAI.ElementaryPositivity.RawShuffle.primitiveCounts_onSlope line 133
13. def OAI.ElementaryPositivity.RawShuffle.primitiveCountsRows line 138
14. lemma OAI.ElementaryPositivity.RawShuffle.primitiveCountsRows_energy line 143
15. lemma OAI.ElementaryPositivity.RawShuffle.primitiveCountsEnergy_admissible line 150
16. def OAI.ElementaryPositivity.RawShuffle.primitiveCountsSeries line 170
17. lemma OAI.ElementaryPositivity.RawShuffle.primitiveCountsSeries_zero line 173