OAI/Combinatorics/Chromatic/Shuffle/PackSplit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.packSplit line 15
  2. lemma OAI.ElementaryPositivity.RawShuffle.packSplit_inl line 22
  3. lemma OAI.ElementaryPositivity.RawShuffle.packSplit_inr line 25
  4. def OAI.ElementaryPositivity.RawShuffle.cutSplit line 28
  5. lemma OAI.ElementaryPositivity.RawShuffle.cutSplit_inl line 33
  6. lemma OAI.ElementaryPositivity.RawShuffle.cutSplit_inr line 36
  7. lemma OAI.ElementaryPositivity.RawShuffle.cutSplit_change line 40
  8. lemma OAI.ElementaryPositivity.RawShuffle.split_symmetric_independent line 60
  9. lemma OAI.ElementaryPositivity.RawShuffle.cutSplit_action line 68
  10. lemma OAI.ElementaryPositivity.RawShuffle.split_symmetric line 93
  11. lemma OAI.ElementaryPositivity.RawShuffle.split_symmetric_span line 108
  12. def OAI.ElementaryPositivity.RawShuffle.firstCut line 125
  13. def OAI.ElementaryPositivity.RawShuffle.localizeS line 128
  14. lemma OAI.ElementaryPositivity.RawShuffle.localizeS_apply line 139
  15. lemma OAI.ElementaryPositivity.RawShuffle.localizeS_injective line 143
  16. def OAI.ElementaryPositivity.RawShuffle.shuffleImage line 148
  17. lemma OAI.ElementaryPositivity.RawShuffle.rawShuffle_mem_localized_image line 151
  18. def OAI.ElementaryPositivity.RawShuffle.tensorShuffle line 157
  19. lemma OAI.ElementaryPositivity.RawShuffle.tensorShuffle_decomposable line 173
  20. lemma OAI.ElementaryPositivity.RawShuffle.tensorShuffle_restricted_mul line 180
  21. theorem OAI.ElementaryPositivity.RawShuffle.mul_shuffle_mem line 198
  22. lemma OAI.ElementaryPositivity.RawShuffle.shuffleImage_mul_mem line 230
  23. theorem OAI.ElementaryPositivity.RawShuffle.destabilizing_mul_mem line 238
  24. def OAI.ElementaryPositivity.RawShuffle.destabilizingIdeal line 256
  25. lemma OAI.ElementaryPositivity.RawShuffle.mem_destabilizingIdeal line 263