OAI/Combinatorics/Chromatic/Shuffle/SameDen.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.sameDen line 15
  2. def OAI.ElementaryPositivity.RawShuffle.arrowNum line 18
  3. lemma OAI.ElementaryPositivity.RawShuffle.kernel_polynomial_ratio line 22
  4. lemma OAI.ElementaryPositivity.RawShuffle.sameDen_union_left line 30
  5. lemma OAI.ElementaryPositivity.RawShuffle.sameDen_union_right line 35
  6. lemma OAI.ElementaryPositivity.RawShuffle.sameDen_ne_zero line 40
  7. lemma OAI.ElementaryPositivity.RawShuffle.sameDen_reverse_dvd line 54
  8. def OAI.ElementaryPositivity.RawShuffle.crossDen line 67
  9. lemma OAI.ElementaryPositivity.RawShuffle.crossDen_dvd line 71
  10. lemma OAI.ElementaryPositivity.RawShuffle.crossDen_ne_zero line 86
  11. lemma OAI.ElementaryPositivity.RawShuffle.crossKernel_polynomial line 93
  12. def OAI.ElementaryPositivity.RawShuffle.crossKernelPolynomial line 115
  13. lemma OAI.ElementaryPositivity.RawShuffle.crossKernelPolynomial_spec line 120
  14. theorem OAI.ElementaryPositivity.RawShuffle.shuffle_grid_cleared line 131
  15. abbrev OAI.ElementaryPositivity.RawShuffle.CutShape line 158
  16. def OAI.ElementaryPositivity.RawShuffle.cutShape line 160
  17. lemma OAI.ElementaryPositivity.RawShuffle.cutShape_eq_iff line 164
  18. def OAI.ElementaryPositivity.RawShuffle.cutByShape line 172
  19. lemma OAI.ElementaryPositivity.RawShuffle.cutByShape_snd line 178
  20. lemma OAI.ElementaryPositivity.RawShuffle.cutByShape_symm line 182
  21. lemma OAI.ElementaryPositivity.RawShuffle.sum_cut_by_shape line 186
  22. lemma OAI.ElementaryPositivity.RawShuffle.sum_grid_by_shape line 192
  23. def OAI.ElementaryPositivity.RawShuffle.shapeComplement line 205
  24. lemma OAI.ElementaryPositivity.RawShuffle.shape_add_complement line 209
  25. def OAI.ElementaryPositivity.RawShuffle.shapeRealization line 214
  26. def OAI.ElementaryPositivity.RawShuffle.shapeCutEquiv line 218