OAI/Combinatorics/Chromatic/Shuffle/SumPackCut.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.sumPackCut line 15
  2. abbrev OAI.ElementaryPositivity.RawShuffle.FourPacks line 30
  3. def OAI.ElementaryPositivity.RawShuffle.canonicalGridCut line 33
  4. def OAI.ElementaryPositivity.RawShuffle.canonicalLeftCut line 36
  5. def OAI.ElementaryPositivity.RawShuffle.canonicalRightCut line 41
  6. def OAI.ElementaryPositivity.RawShuffle.canonicalGridPolynomial line 46
  7. def OAI.ElementaryPositivity.RawShuffle.fourPackAction line 52
  8. lemma OAI.ElementaryPositivity.RawShuffle.gridPolynomial_stabilized line 58
  9. lemma OAI.ElementaryPositivity.RawShuffle.canonicalGridPolynomial_invariant line 74
  10. def OAI.ElementaryPositivity.RawShuffle.fourPackEquiv line 88
  11. def OAI.ElementaryPositivity.RawShuffle.fourGridPolynomial line 103
  12. lemma OAI.ElementaryPositivity.RawShuffle.fourGridPolynomial_invariant line 107
  13. lemma OAI.ElementaryPositivity.RawShuffle.fourGridPolynomial_transfer line 121
  14. lemma OAI.ElementaryPositivity.RawShuffle.gridPolynomial_congr line 137
  15. def OAI.ElementaryPositivity.RawShuffle.gridEmbedding line 155
  16. lemma OAI.ElementaryPositivity.RawShuffle.gridEmbedding_outer_left line 174
  17. lemma OAI.ElementaryPositivity.RawShuffle.gridEmbedding_outer_right line 185
  18. lemma OAI.ElementaryPositivity.RawShuffle.gridEmbedding_cell₁ line 196
  19. lemma OAI.ElementaryPositivity.RawShuffle.gridEmbedding_cell₂ line 210
  20. lemma OAI.ElementaryPositivity.RawShuffle.gridEmbedding_cell₃ line 224
  21. lemma OAI.ElementaryPositivity.RawShuffle.gridEmbedding_cell₄ line 238
  22. lemma OAI.ElementaryPositivity.RawShuffle.gridPolynomial_realization line 251