OAI/Combinatorics/Chromatic/Shuffle/UnitalOriginalDegree.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.unitalSourceFiltration_component_mem line 12
  2. def OAI.ElementaryPositivity.RawShuffle.unitalAssociatedComponent line 24
  3. lemma OAI.ElementaryPositivity.RawShuffle.unitalAssociatedComponent_mk line 30
  4. lemma OAI.ElementaryPositivity.RawShuffle.unitalAssociatedComponent_twice line 37
  5. lemma OAI.ElementaryPositivity.RawShuffle.unitalAssociatedComponent_nonzero line 59
  6. def OAI.ElementaryPositivity.RawShuffle.unitalOriginalHomogeneous line 67
  7. lemma OAI.ElementaryPositivity.RawShuffle.mem_unitalOriginalHomogeneous line 71
  8. lemma OAI.ElementaryPositivity.RawShuffle.unitalOriginalHomogeneous_representative line 75
  9. lemma OAI.ElementaryPositivity.RawShuffle.unitalOriginalHomogeneous_mk line 84
  10. lemma OAI.ElementaryPositivity.RawShuffle.shuffleBUnit_graded line 94
  11. lemma OAI.ElementaryPositivity.RawShuffle.unitalGradeShuffle_original line 104
  12. def OAI.ElementaryPositivity.RawShuffle.globalOriginalHomogeneous line 129
  13. lemma OAI.ElementaryPositivity.RawShuffle.globalOriginalHomogeneous_mul line 134
  14. lemma OAI.ElementaryPositivity.RawShuffle.gradeB_one line 145
  15. lemma OAI.ElementaryPositivity.RawShuffle.globalOriginalHomogeneous_one line 150
  16. lemma OAI.ElementaryPositivity.RawShuffle.localPrimitiveGlobal_original line 154
  17. def OAI.ElementaryPositivity.RawShuffle.globalStringPolynomialDegree line 169
  18. lemma OAI.ElementaryPositivity.RawShuffle.globalStringFamily_original line 172
  19. lemma OAI.ElementaryPositivity.RawShuffle.eulerForm_slopeDimensions_symm line 180
  20. lemma OAI.ElementaryPositivity.RawShuffle.doubleShift_product line 189
  21. def OAI.ElementaryPositivity.RawShuffle.wordPolynomialDegree line 197
  22. lemma OAI.ElementaryPositivity.RawShuffle.primitiveWord_original line 201
  23. lemma OAI.ElementaryPositivity.RawShuffle.wordPolynomialDegree_shift line 211
  24. lemma OAI.ElementaryPositivity.RawShuffle.globalStringPBWBasis_original line 225