OAI/Combinatorics/Chromatic/Shuffle/FourColumns.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.firstColumnAlg line 21
  2. def OAI.ElementaryPositivity.RawShuffle.secondColumnAlg line 25
  3. def OAI.ElementaryPositivity.RawShuffle.crossingColumnAlg line 29
  4. def OAI.ElementaryPositivity.RawShuffle.crossingColumnVars line 33
  5. lemma OAI.ElementaryPositivity.RawShuffle.fourValue_firstColumn line 38
  6. lemma OAI.ElementaryPositivity.RawShuffle.fourValue_secondColumn line 53
  7. lemma OAI.ElementaryPositivity.RawShuffle.fourValue_crossingColumn line 68
  8. lemma OAI.ElementaryPositivity.RawShuffle.fourColumns_product line 82
  9. lemma OAI.ElementaryPositivity.RawShuffle.rawKernel_rename line 90
  10. def OAI.ElementaryPositivity.TensorPolynomials.tensorPolynomial line 108
  11. lemma OAI.ElementaryPositivity.TensorPolynomials.tensorPolynomial_tmul line 114
  12. lemma OAI.ElementaryPositivity.TensorPolynomials.eval_map line 121
  13. lemma OAI.ElementaryPositivity.TensorPolynomials.tensorPolynomial_eval line 130
  14. def OAI.ElementaryPositivity.RawShuffle.commonTaylorTensor line 164
  15. lemma OAI.ElementaryPositivity.RawShuffle.commonTaylorTensor_eval line 169
  16. lemma OAI.ElementaryPositivity.RawShuffle.map_commonTaylorTensor line 175
  17. def OAI.ElementaryPositivity.RawShuffle.fourRelativeTaylor line 186
  18. lemma OAI.ElementaryPositivity.RawShuffle.fourRelativeTaylor_eval line 192
  19. lemma OAI.ElementaryPositivity.RawShuffle.fourRelativeTaylor_tmul line 201
  20. lemma OAI.ElementaryPositivity.RawShuffle.fourRelativeRaw_left line 215
  21. lemma OAI.ElementaryPositivity.RawShuffle.fourRelativeRaw_right line 227
  22. lemma OAI.ElementaryPositivity.RawShuffle.map_commonTaylorTensor_left line 238
  23. lemma OAI.ElementaryPositivity.RawShuffle.map_fourRelativeTaylor line 253