OAI/Combinatorics/Chromatic/Shuffle/Diagonal.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.ShufflePolynomiality.diagonal line 12
  2. def OAI.ElementaryPositivity.ShufflePolynomiality.merge line 14
  3. def OAI.ElementaryPositivity.ShufflePolynomiality.identify line 16
  4. lemma OAI.ElementaryPositivity.ShufflePolynomiality.merge_left line 19
  5. lemma OAI.ElementaryPositivity.ShufflePolynomiality.merge_right line 22
  6. lemma OAI.ElementaryPositivity.ShufflePolynomiality.identify_diagonal line 25
  7. lemma OAI.ElementaryPositivity.ShufflePolynomiality.diagonal_dvd_sub_identify line 28
  8. lemma OAI.ElementaryPositivity.ShufflePolynomiality.diagonal_dvd_iff_identify_eq_zero line 47
  9. lemma OAI.ElementaryPositivity.ShufflePolynomiality.ker_identify line 55
  10. lemma OAI.ElementaryPositivity.ShufflePolynomiality.diagonal_ne_zero line 61
  11. lemma OAI.ElementaryPositivity.ShufflePolynomiality.diagonal_prime line 64
  12. lemma OAI.ElementaryPositivity.ShufflePolynomiality.merge_equal_for_ordered_pair line 72
  13. lemma OAI.ElementaryPositivity.ShufflePolynomiality.diagonals_not_dvd line 88
  14. lemma OAI.ElementaryPositivity.ShufflePolynomiality.diagonals_isRelPrime line 99
  15. theorem OAI.ElementaryPositivity.ShufflePolynomiality.diagonal_powers_product_dvd line 104
  16. lemma OAI.ElementaryPositivity.ShufflePolynomiality.merge_swap line 114
  17. theorem OAI.ElementaryPositivity.ShufflePolynomiality.diagonal_dvd_of_antisymmetric line 124
  18. theorem OAI.ElementaryPositivity.ShufflePolynomiality.vandermonde_dvd line 134
  19. def OAI.ElementaryPositivity.ShufflePolynomiality.alternate line 150
  20. lemma OAI.ElementaryPositivity.ShufflePolynomiality.rename_alternate_of_sign_neg line 155
  21. lemma OAI.ElementaryPositivity.ShufflePolynomiality.diagonal_dvd_alternate line 171
  22. theorem OAI.ElementaryPositivity.ShufflePolynomiality.same_pack_alternation_polynomial line 179
  23. lemma OAI.ElementaryPositivity.ShufflePolynomiality.merge_equal_pair line 195
  24. lemma OAI.ElementaryPositivity.ShufflePolynomiality.independent_diagonals line 211
  25. theorem OAI.ElementaryPositivity.ShufflePolynomiality.pair_powers_product_dvd line 223
  26. def OAI.ElementaryPositivity.ShufflePolynomiality.packAction line 245
  27. def OAI.ElementaryPositivity.ShufflePolynomiality.packSign line 250
  28. lemma OAI.ElementaryPositivity.ShufflePolynomiality.packAction_transposition line 262
  29. lemma OAI.ElementaryPositivity.ShufflePolynomiality.packSign_transposition line 279
  30. lemma OAI.ElementaryPositivity.ShufflePolynomiality.pack_alternate_diagonal line 290
  31. def OAI.ElementaryPositivity.ShufflePolynomiality.packPairs line 299
  32. def OAI.ElementaryPositivity.ShufflePolynomiality.packVandermonde line 306
  33. theorem OAI.ElementaryPositivity.ShufflePolynomiality.pack_alternation_polynomial line 310
  34. def OAI.ElementaryPositivity.ShufflePolynomiality.naturalVandermonde line 343
  35. def OAI.ElementaryPositivity.ShufflePolynomiality.finPackPair line 347
  36. lemma OAI.ElementaryPositivity.ShufflePolynomiality.finPackPair_injective line 352
  37. def OAI.ElementaryPositivity.ShufflePolynomiality.naturalPairs line 360
  38. lemma OAI.ElementaryPositivity.ShufflePolynomiality.naturalVandermonde_product line 365
  39. lemma OAI.ElementaryPositivity.ShufflePolynomiality.rename_naturalVandermonde line 379
  40. lemma OAI.ElementaryPositivity.ShufflePolynomiality.naturalVandermonde_dvd_alternate line 403