OAI/Combinatorics/Chromatic/Shuffle/GlobalCoproductCoassociative.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.globalTripleCoproduct line 15
  2. def OAI.ElementaryPositivity.RawShuffle.globalLeftTripleOutput line 29
  3. def OAI.ElementaryPositivity.RawShuffle.globalLeftTripleCoproduct line 39
  4. lemma OAI.ElementaryPositivity.RawShuffle.globalTripleCoproduct_left_explicit line 46
  5. lemma OAI.ElementaryPositivity.RawShuffle.globalTripleCoproduct_left line 68
  6. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCast_refl line 77
  7. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeCoproduct_comp_cast_refl line 81
  8. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorGrade_coproduct_family_cast line 88
  9. lemma OAI.ElementaryPositivity.RawShuffle.globalTripleGrade_left_cast_natural line 98
  10. lemma OAI.ElementaryPositivity.RawShuffle.globalTripleGrade_right_cast_natural line 115
  11. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedLeftSplit_dimensions line 131
  12. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedRightSplit_dimensions line 153
  13. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedLeftSplit_natural line 175
  14. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedRightSplit_natural line 189
  15. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedLeftSplit_build_left line 206
  16. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedLeftSplit_build line 220
  17. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedRightSplit_build line 231
  18. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedLeftSplit_view line 246
  19. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedRightSplit_view line 257
  20. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedLeft_sum line 268
  21. lemma OAI.ElementaryPositivity.RawShuffle.globalIteratedRight_sum line 283
  22. lemma OAI.ElementaryPositivity.RawShuffle.globalCoproduct_coassociative_lof line 296
  23. theorem OAI.ElementaryPositivity.RawShuffle.globalCoproduct_coassociative line 308