OAI/Combinatorics/Chromatic/Shuffle/TensorColumnNaturality.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.TensorColumns.map_first line 16
2. lemma OAI.ElementaryPositivity.TensorColumns.map_second line 24
3. lemma OAI.ElementaryPositivity.TensorColumns.map_middle line 32
4. def OAI.ElementaryPositivity.RawShuffle.firstColumnBAlg line 69
5. def OAI.ElementaryPositivity.RawShuffle.secondColumnBAlg line 72
6. lemma OAI.ElementaryPositivity.RawShuffle.fourQuotient_firstColumn line 76
7. lemma OAI.ElementaryPositivity.RawShuffle.fourQuotient_secondColumn line 83
8. lemma OAI.ElementaryPositivity.RawShuffle.fourQuotient_crossingColumn line 90
9. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesQuotient_firstColumn line 97
10. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesQuotient_secondColumn line 107
11. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesQuotient_crossingUnit line 117
12. lemma OAI.ElementaryPositivity.RawShuffle.unit_map_ratio_square line 127
13. lemma OAI.ElementaryPositivity.RawShuffle.fourSeriesQuotient_crossingRatio line 136
14. lemma OAI.ElementaryPositivity.RawShuffle.fourInputSeriesB_mk line 147