OAI/Combinatorics/Chromatic/Shuffle/Interaction.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.interaction line 14
  2. lemma OAI.ElementaryPositivity.RawShuffle.interaction_nonnegative line 18
  3. lemma OAI.ElementaryPositivity.RawShuffle.interaction_add line 23
  4. lemma OAI.ElementaryPositivity.RawShuffle.eulerForm_lower line 30
  5. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.doubleShift_lower line 36
  6. def OAI.ElementaryPositivity.RawShuffle.dimensionEquivB line 47
  7. def OAI.ElementaryPositivity.RawShuffle.restrictionTest line 52
  8. def OAI.ElementaryPositivity.RawShuffle.sourceFiltration line 62
  9. lemma OAI.ElementaryPositivity.RawShuffle.sourceFiltration_antitone line 77
  10. theorem OAI.ElementaryPositivity.RawShuffle.sourceFiltration_lower line 82
  11. lemma OAI.ElementaryPositivity.RawShuffle.coeff_zero_toMvPolynomial line 98
  12. lemma OAI.ElementaryPositivity.RawShuffle.restrictionTest_leaf_zero line 105
  13. theorem OAI.ElementaryPositivity.RawShuffle.sourceFiltration_upper line 113
  14. theorem OAI.ElementaryPositivity.RawShuffle.leading_restrictions_detect line 124
  15. lemma OAI.ElementaryPositivity.RawShuffle.reynoldsS_homogeneous line 143
  16. lemma OAI.ElementaryPositivity.RawShuffle.separateTensor_product_any line 151
  17. lemma OAI.ElementaryPositivity.RawShuffle.monomial_sumElim line 157
  18. lemma OAI.ElementaryPositivity.RawShuffle.totalWeight_sumElim line 161
  19. lemma OAI.ElementaryPositivity.RawShuffle.component_separateTensor_homogeneous line 166
  20. lemma OAI.ElementaryPositivity.RawShuffle.component_restrictTensor_homogeneous line 185
  21. lemma OAI.ElementaryPositivity.RawShuffle.component_quotientTensor line 191
  22. theorem OAI.ElementaryPositivity.RawShuffle.restrictionB_graded line 199