OAI/Combinatorics/Chromatic/Shuffle/Realization.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.RawShuffle.Realization line 14
  2. def OAI.ElementaryPositivity.RawShuffle.realizationMap line 16
  3. lemma OAI.ElementaryPositivity.RawShuffle.realizationMap_injective line 20
  4. lemma OAI.ElementaryPositivity.RawShuffle.rename_realization_independent line 26
  5. def OAI.ElementaryPositivity.RawShuffle.valueAt line 36
  6. lemma OAI.ElementaryPositivity.RawShuffle.valueAt_independent line 41
  7. def OAI.ElementaryPositivity.RawShuffle.defaultRealization line 45
  8. def OAI.ElementaryPositivity.RawShuffle.labeledValue line 49
  9. lemma OAI.ElementaryPositivity.RawShuffle.labeledValue_eq line 54
  10. lemma OAI.ElementaryPositivity.RawShuffle.valueAt_shuffle line 62
  11. abbrev OAI.ElementaryPositivity.RawShuffle.SizedCut line 78
  12. def OAI.ElementaryPositivity.RawShuffle.cutRealizationEquiv line 81
  13. lemma OAI.ElementaryPositivity.RawShuffle.cutRealizationEquiv_left line 87
  14. lemma OAI.ElementaryPositivity.RawShuffle.cutRealizationEquiv_right line 92
  15. def OAI.ElementaryPositivity.RawShuffle.leftRealization line 97
  16. def OAI.ElementaryPositivity.RawShuffle.rightRealization line 103
  17. lemma OAI.ElementaryPositivity.RawShuffle.leftRealization_map line 110
  18. lemma OAI.ElementaryPositivity.RawShuffle.rightRealization_map line 114
  19. lemma OAI.ElementaryPositivity.RawShuffle.labeledValue_left line 119
  20. lemma OAI.ElementaryPositivity.RawShuffle.labeledValue_right line 126
  21. def OAI.ElementaryPositivity.RawShuffle.pairKernel line 133
  22. lemma OAI.ElementaryPositivity.RawShuffle.kernel_formula line 139
  23. lemma OAI.ElementaryPositivity.RawShuffle.mapped_cut_kernel line 160
  24. lemma OAI.ElementaryPositivity.RawShuffle.valueAt_shuffle_sum line 176
  25. lemma OAI.ElementaryPositivity.RawShuffle.cut_right_card line 198
  26. lemma OAI.ElementaryPositivity.RawShuffle.cut_card_add line 211
  27. lemma OAI.ElementaryPositivity.RawShuffle.pack_shuffle_sum line 220
  28. lemma OAI.ElementaryPositivity.RawShuffle.labeledValue_shuffle line 241
  29. lemma OAI.ElementaryPositivity.RawShuffle.valueAt_injective line 260
  30. lemma OAI.ElementaryPositivity.RawShuffle.labeledValue_injective line 268
  31. def OAI.ElementaryPositivity.RawShuffle.castS line 274
  32. lemma OAI.ElementaryPositivity.RawShuffle.labeledValue_cast line 277
  33. theorem OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_assoc line 282