OAI/Combinatorics/Chromatic/Shuffle/InputProduct.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.WeightedTorusSeries.crossInteraction_axis line 16
  2. lemma OAI.ElementaryPositivity.WeightedTorusSeries.partialCoefficient_singleton line 30
  3. lemma OAI.ElementaryPositivity.WeightedTorusSeries.push_partial_axis line 41
  4. lemma OAI.ElementaryPositivity.WeightedTorusSeries.push_partial_axis_family line 46
  5. def OAI.ElementaryPositivity.RawShuffle.literalAxisScalar line 63
  6. def OAI.ElementaryPositivity.RawShuffle.literalAxis line 66
  7. lemma OAI.ElementaryPositivity.RawShuffle.partial_univ_literal line 70
  8. theorem OAI.ElementaryPositivity.RawShuffle.literalInput_ordered line 80
  9. def OAI.ElementaryPositivity.RawShuffle.geometricQuiver line 105
  10. def OAI.ElementaryPositivity.RawShuffle.rootSum line 108
  11. lemma OAI.ElementaryPositivity.RawShuffle.rootSum_single line 113
  12. lemma OAI.ElementaryPositivity.RawShuffle.geometricQuiver_diag line 118
  13. lemma OAI.ElementaryPositivity.RawShuffle.geometricQuiver_skew line 124
  14. lemma OAI.ElementaryPositivity.RawShuffle.geometricQuiver_euler line 133
  15. lemma OAI.ElementaryPositivity.RawShuffle.geometricQuiver_forward line 150
  16. lemma OAI.ElementaryPositivity.RawShuffle.geometricQuiver_pairwise line 157
  17. lemma OAI.ElementaryPositivity.RawShuffle.geometricQuiver_symmetric line 165