OAI/Combinatorics/Chromatic/Shuffle/ReynoldsS.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.reynoldsS line 13
  2. lemma OAI.ElementaryPositivity.RawShuffle.reynoldsS_val line 20
  3. lemma OAI.ElementaryPositivity.RawShuffle.tensorEquivSum_tmul line 24
  4. def OAI.ElementaryPositivity.RawShuffle.tensorValue line 39
  5. lemma OAI.ElementaryPositivity.RawShuffle.tensorValue_tmul line 45
  6. def OAI.ElementaryPositivity.RawShuffle.separateTensor line 49
  7. lemma OAI.ElementaryPositivity.RawShuffle.separateTensor_product line 54
  8. lemma OAI.ElementaryPositivity.RawShuffle.separateTensor_tensorValue line 59
  9. lemma OAI.ElementaryPositivity.RawShuffle.tensorValue_injective line 65
  10. lemma OAI.ElementaryPositivity.RawShuffle.tensorValue_separateTensor line 69
  11. def OAI.ElementaryPositivity.RawShuffle.restrictTensor line 87
  12. lemma OAI.ElementaryPositivity.RawShuffle.tensorValue_restrictTensor line 91
  13. lemma OAI.ElementaryPositivity.RawShuffle.restrictTensor_independent line 95
  14. def OAI.ElementaryPositivity.RawShuffle.restrictQuotientAt line 104
  15. lemma OAI.ElementaryPositivity.RawShuffle.restrictQuotientAt_independent line 111