OAI/Combinatorics/Chromatic/Shuffle/GlobalTensorGradeProduct.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.slopeDimensions_onSlope line 15
2. lemma OAI.ElementaryPositivity.RawShuffle.slopeDimensions_cellsOnSlope line 19
3. lemma OAI.ElementaryPositivity.RawShuffle.unitalLof_cast line 25
4. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorGradeInclusion_cast line 34
5. lemma OAI.ElementaryPositivity.RawShuffle.unitalLof_shuffle line 45
6. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorGradeInclusion_part_add line 55
7. theorem OAI.ElementaryPositivity.RawShuffle.globalTensorGradeInclusion_signedProduct line 67
8. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorGradeInclusion_signedProduct_cast line 95
9. lemma OAI.ElementaryPositivity.RawShuffle.globalRawColumnProduct line 112
10. def OAI.ElementaryPositivity.RawShuffle.unitalTensorGradeComm line 140
11. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct_cocommutative line 146
12. lemma OAI.ElementaryPositivity.RawShuffle.unitalTensorGradeComm_part line 184
13. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorGradeInclusion_comm line 203