OAI/Combinatorics/Chromatic/Shuffle/GlobalPBWBasis.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveFamily_span line 16
  2. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveFamily_adjoin line 24
  3. lemma OAI.ElementaryPositivity.RawShuffle.primitive_mem_wordLength_one line 37
  4. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveWords_span line 43
  5. def OAI.ElementaryPositivity.RawShuffle.globalPBWBasis line 79
  6. lemma OAI.ElementaryPositivity.RawShuffle.globalPBWBasis_apply line 85
  7. lemma OAI.ElementaryPositivity.RawShuffle.globalPBWBasis_homogeneous line 90
  8. def OAI.ElementaryPositivity.RawShuffle.primitiveBasisRetraction line 113
  9. lemma OAI.ElementaryPositivity.RawShuffle.primitiveBasisRetraction_unit line 120
  10. lemma OAI.ElementaryPositivity.RawShuffle.primitiveBasisRetraction_apply line 128
  11. def OAI.ElementaryPositivity.RawShuffle.primitiveBasisDual line 134
  12. lemma OAI.ElementaryPositivity.RawShuffle.primitiveBasisDual_unit line 138
  13. lemma OAI.ElementaryPositivity.RawShuffle.primitiveBasisDual_apply line 145
  14. lemma OAI.ElementaryPositivity.RawShuffle.primitiveBasisFamilyWords_independent line 154
  15. lemma OAI.ElementaryPositivity.RawShuffle.primitiveBasisFamily_adjoin line 162
  16. lemma OAI.ElementaryPositivity.RawShuffle.primitiveBasisFamily_wordLength line 177
  17. lemma OAI.ElementaryPositivity.RawShuffle.primitiveBasisFamilyWords_span line 184
  18. def OAI.ElementaryPositivity.RawShuffle.primitiveBasisPBW line 218
  19. lemma OAI.ElementaryPositivity.RawShuffle.primitiveBasisPBW_apply line 222