OAI/Combinatorics/Chromatic/Shuffle/GlobalConvolutionSeries.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.convSeries line 18
  2. lemma OAI.ElementaryPositivity.RawShuffle.convSeries_lof line 23
  3. lemma OAI.ElementaryPositivity.RawShuffle.convolutionProjection_series line 31
  4. lemma OAI.ElementaryPositivity.RawShuffle.convolutionProjection_jointly_injective line 47
  5. lemma OAI.ElementaryPositivity.RawShuffle.convSeries_post line 57
  6. lemma OAI.ElementaryPositivity.RawShuffle.convSeries_order_one line 68
  7. lemma OAI.ElementaryPositivity.RawShuffle.convVanishes_one_add_product line 76
  8. lemma OAI.ElementaryPositivity.RawShuffle.convSeries_log_product line 83
  9. def OAI.ElementaryPositivity.RawShuffle.signedLeft line 109
  10. def OAI.ElementaryPositivity.RawShuffle.signedRight line 111
  11. lemma OAI.ElementaryPositivity.RawShuffle.signedLeft_apply line 114
  12. lemma OAI.ElementaryPositivity.RawShuffle.signedRight_apply line 116
  13. def OAI.ElementaryPositivity.RawShuffle.signedMapProduct line 119
  14. lemma OAI.ElementaryPositivity.RawShuffle.signedMapProduct_tmul line 123
  15. lemma OAI.ElementaryPositivity.RawShuffle.signedTensor_mul_eq line 127
  16. lemma OAI.ElementaryPositivity.RawShuffle.signedLeft_product line 130
  17. lemma OAI.ElementaryPositivity.RawShuffle.signedRight_product line 143
  18. lemma OAI.ElementaryPositivity.RawShuffle.signedLeftRight_product line 156
  19. lemma OAI.ElementaryPositivity.RawShuffle.signedRightLeft_product line 168
  20. def OAI.ElementaryPositivity.RawShuffle.signedLeftAlgHom line 183
  21. def OAI.ElementaryPositivity.RawShuffle.signedRightAlgHom line 186