OAI/Combinatorics/Chromatic/Shuffle/DimensionGrid.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElementaryPositivity.RawShuffle.DimensionSplit line 9
2. def OAI.ElementaryPositivity.RawShuffle.DimensionSplit.left line 13
3. def OAI.ElementaryPositivity.RawShuffle.DimensionSplit.right line 14
4. lemma OAI.ElementaryPositivity.RawShuffle.DimensionSplit.left_add_right line 16
5. lemma OAI.ElementaryPositivity.RawShuffle.DimensionSplit.ext line 22
6. def OAI.ElementaryPositivity.RawShuffle.DimensionSplit.ofPair line 26
7. lemma OAI.ElementaryPositivity.RawShuffle.DimensionSplit.left_ofPair line 29
8. lemma OAI.ElementaryPositivity.RawShuffle.DimensionSplit.right_ofPair line 32
9. lemma OAI.ElementaryPositivity.RawShuffle.DimensionSplit.ofPair_left_right line 40
10. def OAI.ElementaryPositivity.RawShuffle.DimensionSplit.pairEquiv line 45
11. abbrev OAI.ElementaryPositivity.RawShuffle.RowDimensionGrid line 55
12. abbrev OAI.ElementaryPositivity.RawShuffle.ColumnDimensionGrid line 59
13. def OAI.ElementaryPositivity.RawShuffle.transposeDimensionGrid line 63
14. lemma OAI.ElementaryPositivity.RawShuffle.transposeDimensionGrid_first_left line 84
15. lemma OAI.ElementaryPositivity.RawShuffle.transposeDimensionGrid_first_right line 88
16. lemma OAI.ElementaryPositivity.RawShuffle.transposeDimensionGrid_second_left line 93
17. lemma OAI.ElementaryPositivity.RawShuffle.transposeDimensionGrid_second_right line 97
18. lemma OAI.ElementaryPositivity.RawShuffle.sum_transposeDimensionGrid line 104
19. lemma OAI.ElementaryPositivity.RawShuffle.sum_transposeDimensionGrid_congr line 111
20. lemma OAI.ElementaryPositivity.RawShuffle.subtypePair_heq line 132
21. def OAI.ElementaryPositivity.RawShuffle.dimensionProduct line 141