OAI/Combinatorics/Chromatic/Shuffle/GridQuotient.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.shuffleTensorBUnit line 31
  2. lemma OAI.ElementaryPositivity.RawShuffle.quotient_shuffleTensorUnit line 36
  3. def OAI.ElementaryPositivity.RawShuffle.fourQuotient line 44
  4. def OAI.ElementaryPositivity.RawShuffle.fourInterchangeB line 49
  5. lemma OAI.ElementaryPositivity.RawShuffle.fourQuotient_interchange line 54
  6. lemma OAI.ElementaryPositivity.RawShuffle.quotient_twoTargetTransfer_unit line 63
  7. lemma OAI.ElementaryPositivity.RawShuffle.fourQuotient_grid_factor line 84
  8. def OAI.ElementaryPositivity.TensorColumns.first line 112
  9. def OAI.ElementaryPositivity.TensorColumns.second line 114
  10. lemma OAI.ElementaryPositivity.TensorColumns.first_tmul line 117
  11. lemma OAI.ElementaryPositivity.TensorColumns.second_tmul line 119
  12. lemma OAI.ElementaryPositivity.TensorColumns.product line 122