OAI/Combinatorics/Chromatic/Shuffle/GlobalPBWIndependent.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.RawShuffle.PBWWord line 17
  2. theorem OAI.ElementaryPositivity.RawShuffle.globalPBW_independent line 20
  3. def OAI.ElementaryPositivity.RawShuffle.globalPrimitiveProjection line 55
  4. lemma OAI.ElementaryPositivity.RawShuffle.globalPrimitiveProjection_restrict line 59
  5. lemma OAI.ElementaryPositivity.RawShuffle.globalPrimitiveProjection_unit line 63
  6. def OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitives line 71
  7. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitives_span line 74
  8. def OAI.ElementaryPositivity.RawShuffle.PrimitiveIndex line 89
  9. def OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveBasis line 93
  10. def OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveFamily line 97
  11. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveFamily_primitive line 100
  12. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveFamily_exists_weight line 104
  13. def OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveWeight line 108
  14. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveFamily_weight line 111
  15. def OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveDual line 116
  16. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveDual_unit line 120
  17. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveDual_apply line 125
  18. instance OAI.ElementaryPositivity.RawShuffle.primitiveIndexLinearOrder line 133
  19. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveWords_independent line 136