OAI/Combinatorics/Chromatic/Shuffle/Cut.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.Cut line 13
  2. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 15) line 15
  3. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 16) line 16
  4. def OAI.ElementaryPositivity.RawShuffle.cutPerm line 20
  5. lemma OAI.ElementaryPositivity.RawShuffle.cutPerm_val line 25
  6. lemma OAI.ElementaryPositivity.RawShuffle.mem_cutPerm line 29
  7. def OAI.ElementaryPositivity.RawShuffle.leftEnum line 34
  8. lemma OAI.ElementaryPositivity.RawShuffle.right_card line 38
  9. def OAI.ElementaryPositivity.RawShuffle.rightEnum line 41
  10. def OAI.ElementaryPositivity.RawShuffle.leftInput line 44
  11. def OAI.ElementaryPositivity.RawShuffle.rightInput line 47
  12. def OAI.ElementaryPositivity.RawShuffle.leftImageEquiv line 50
  13. def OAI.ElementaryPositivity.RawShuffle.rightImageEquiv line 54
  14. def OAI.ElementaryPositivity.RawShuffle.leftReindex line 58
  15. def OAI.ElementaryPositivity.RawShuffle.rightReindex line 62
  16. lemma OAI.ElementaryPositivity.RawShuffle.leftInput_reindex line 67
  17. lemma OAI.ElementaryPositivity.RawShuffle.rightInput_reindex line 77
  18. def OAI.ElementaryPositivity.RawShuffle.PackSymmetric line 86
  19. lemma OAI.ElementaryPositivity.RawShuffle.rename_leftInput line 90
  20. lemma OAI.ElementaryPositivity.RawShuffle.rename_rightInput line 97
  21. lemma OAI.ElementaryPositivity.RawShuffle.cutPerm_compl line 104
  22. def OAI.ElementaryPositivity.RawShuffle.cutFactor line 114
  23. lemma OAI.ElementaryPositivity.RawShuffle.rename_cutFactor line 118
  24. def OAI.ElementaryPositivity.RawShuffle.cutDenominator line 128
  25. def OAI.ElementaryPositivity.RawShuffle.cutNumerator line 130
  26. lemma OAI.ElementaryPositivity.RawShuffle.rename_cutDenominator line 135
  27. lemma OAI.ElementaryPositivity.RawShuffle.rename_cutNumerator line 141
  28. lemma OAI.ElementaryPositivity.RawShuffle.cutDenominator_dvd line 150
  29. lemma OAI.ElementaryPositivity.RawShuffle.cutDenominator_ne_zero line 172
  30. def OAI.ElementaryPositivity.RawShuffle.rawShuffle line 176
  31. lemma OAI.ElementaryPositivity.RawShuffle.rawShuffle_symmetric line 181
  32. lemma OAI.ElementaryPositivity.RawShuffle.rawShuffle_regular line 192
  33. theorem OAI.ElementaryPositivity.RawShuffle.rawShuffle_polynomial line 213