OAI/Combinatorics/Chromatic/Shuffle/SignedTensorGradeProduct.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.signedCellMultiplyB line 14
  2. lemma OAI.ElementaryPositivity.RawShuffle.signedCellMultiplyB_apply line 25
  3. lemma OAI.ElementaryPositivity.RawShuffle.signedCellMultiplyB_filtered line 36
  4. def OAI.ElementaryPositivity.RawShuffle.signedCellGradeMultiply line 53
  5. lemma OAI.ElementaryPositivity.RawShuffle.signedCellGradeMultiply_mk line 72
  6. def OAI.ElementaryPositivity.RawShuffle.unitalTensorFiltrationCast line 94
  7. def OAI.ElementaryPositivity.RawShuffle.unitalTensorGradeCast line 102
  8. lemma OAI.ElementaryPositivity.RawShuffle.unitalTensorFiltrationCast_val line 110
  9. lemma OAI.ElementaryPositivity.RawShuffle.unitalTensorGradeCast_mk line 119
  10. def OAI.ElementaryPositivity.RawShuffle.splitCoproductFiltration line 129
  11. def OAI.ElementaryPositivity.RawShuffle.splitCoproductGrade line 139
  12. lemma OAI.ElementaryPositivity.RawShuffle.splitCoproductGrade_mk line 147
  13. lemma OAI.ElementaryPositivity.RawShuffle.splitCoproductFiltration_val line 157
  14. lemma OAI.ElementaryPositivity.RawShuffle.splitCoproductFiltration_val_mk line 168
  15. def OAI.ElementaryPositivity.RawShuffle.columnFiltrationTerm line 178
  16. def OAI.ElementaryPositivity.RawShuffle.columnGradeTerm line 194
  17. lemma OAI.ElementaryPositivity.RawShuffle.columnGradeTerm_mk line 207
  18. lemma OAI.ElementaryPositivity.RawShuffle.columnFiltrationTerm_val_mk line 220
  19. theorem OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct_shuffle_column line 238