OAI/Combinatorics/Chromatic/Shuffle/CellVars.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.RawShuffle.CellVars line 13
  2. abbrev OAI.ElementaryPositivity.RawShuffle.CellGroup line 14
  3. def OAI.ElementaryPositivity.RawShuffle.cellAction line 17
  4. def OAI.ElementaryPositivity.RawShuffle.fourValue line 20
  5. lemma OAI.ElementaryPositivity.RawShuffle.fourValue_tmul line 26
  6. def OAI.ElementaryPositivity.RawShuffle.separateFour line 34
  7. lemma OAI.ElementaryPositivity.RawShuffle.separateFour_product line 40
  8. lemma OAI.ElementaryPositivity.RawShuffle.fourValue_separateFour line 47
  9. lemma OAI.ElementaryPositivity.RawShuffle.separateFour_fourValue line 62
  10. lemma OAI.ElementaryPositivity.RawShuffle.fourValue_injective line 69
  11. def OAI.ElementaryPositivity.RawShuffle.cellTransfer line 73
  12. lemma OAI.ElementaryPositivity.RawShuffle.quotient_cellTransfer_zero line 78
  13. def OAI.ElementaryPositivity.RawShuffle.renameInjFraction line 94
  14. lemma OAI.ElementaryPositivity.RawShuffle.renameInjFraction_algebraMap line 100
  15. def OAI.ElementaryPositivity.RawShuffle.localizeTensor line 107
  16. lemma OAI.ElementaryPositivity.RawShuffle.localizeTensor_injective line 117
  17. def OAI.ElementaryPositivity.RawShuffle.cutKernel line 122
  18. lemma OAI.ElementaryPositivity.RawShuffle.tensorShuffle_kernel line 127
  19. def OAI.ElementaryPositivity.RawShuffle.doubleTensorShuffle line 132
  20. lemma OAI.ElementaryPositivity.RawShuffle.doubleTensorShuffle_product line 148
  21. lemma OAI.ElementaryPositivity.RawShuffle.doubleTensorShuffle_fourValue line 167
  22. lemma OAI.ElementaryPositivity.RawShuffle.doubleTensorShuffle_invariant line 187