OAI/Combinatorics/Chromatic/Shuffle/GlobalPrimitiveBracket.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.globalColorSign line 16
  2. lemma OAI.ElementaryPositivity.RawShuffle.globalColorSign_symm line 19
  3. lemma OAI.ElementaryPositivity.RawShuffle.globalColorSign_sq line 30
  4. lemma OAI.ElementaryPositivity.RawShuffle.globalColorSign_zero_left line 36
  5. lemma OAI.ElementaryPositivity.RawShuffle.globalColorSign_zero_right line 39
  6. lemma OAI.ElementaryPositivity.RawShuffle.globalHomogeneous_one line 43
  7. lemma OAI.ElementaryPositivity.RawShuffle.signedTensor_mul_homogeneous line 46
  8. lemma OAI.ElementaryPositivity.RawShuffle.globalPrimitive_product_coproduct line 58
  9. theorem OAI.ElementaryPositivity.RawShuffle.globalPrimitive_bracket line 82
  10. theorem OAI.ElementaryPositivity.RawShuffle.globalPrimitive_odd_square line 96
  11. structure OAI.ElementaryPositivity.RawShuffle.SignedWordCut line 119
  12. def OAI.ElementaryPositivity.RawShuffle.wordWeight line 124
  13. def OAI.ElementaryPositivity.RawShuffle.primitiveWord line 125
  14. def OAI.ElementaryPositivity.RawShuffle.SignedWordCut.prependLeft line 127
  15. def OAI.ElementaryPositivity.RawShuffle.SignedWordCut.prependRight line 129
  16. def OAI.ElementaryPositivity.RawShuffle.signedWordCuts line 133
  17. lemma OAI.ElementaryPositivity.RawShuffle.primitiveWord_nil line 138
  18. lemma OAI.ElementaryPositivity.RawShuffle.primitiveWord_cons line 139
  19. lemma OAI.ElementaryPositivity.RawShuffle.primitiveWord_homogeneous line 142
  20. lemma OAI.ElementaryPositivity.RawShuffle.signedWordCuts_lengths line 151
  21. lemma OAI.ElementaryPositivity.RawShuffle.signedWordCuts_sublist line 167
  22. def OAI.ElementaryPositivity.RawShuffle.wordCutTensor line 178
  23. lemma OAI.ElementaryPositivity.RawShuffle.wordCutTensor_left line 182
  24. lemma OAI.ElementaryPositivity.RawShuffle.wordCutTensor_right line 194
  25. theorem OAI.ElementaryPositivity.RawShuffle.globalCoproduct_primitiveWord line 206