OAI/Combinatorics/Chromatic/Shuffle/GlobalPrimitiveStrings.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.RawShuffle.NonzeroSlopeWeight line 19
  2. def OAI.ElementaryPositivity.RawShuffle.localPrimitiveInclusion line 21
  3. lemma OAI.ElementaryPositivity.RawShuffle.localPrimitiveInclusion_injective line 27
  4. def OAI.ElementaryPositivity.RawShuffle.localPrimitiveGlobal line 31
  5. lemma OAI.ElementaryPositivity.RawShuffle.localPrimitiveGlobal_mem line 35
  6. def OAI.ElementaryPositivity.RawShuffle.localPrimitiveSumToGlobal line 44
  7. lemma OAI.ElementaryPositivity.RawShuffle.localPrimitiveSumToGlobal_injective line 50
  8. lemma OAI.ElementaryPositivity.RawShuffle.localPrimitiveSumToGlobal_lof line 54
  9. abbrev OAI.ElementaryPositivity.RawShuffle.GlobalStringIndex line 65
  10. def OAI.ElementaryPositivity.RawShuffle.globalStringFamily line 68
  11. lemma OAI.ElementaryPositivity.RawShuffle.globalStringFamily_mem line 72
  12. lemma OAI.ElementaryPositivity.RawShuffle.globalStringFamily_weight line 76
  13. lemma OAI.ElementaryPositivity.RawShuffle.globalStringFamily_independent line 80
  14. lemma OAI.ElementaryPositivity.RawShuffle.localPrimitiveGlobal_mem_span line 94
  15. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitive_mem_stringSpan line 106
  16. lemma OAI.ElementaryPositivity.RawShuffle.globalStringFamily_span line 122
  17. instance OAI.ElementaryPositivity.RawShuffle.globalStringIndexLinearOrder line 154
  18. def OAI.ElementaryPositivity.RawShuffle.globalStringPBWBasis line 157
  19. lemma OAI.ElementaryPositivity.RawShuffle.globalStringPBWBasis_apply line 164
  20. lemma OAI.ElementaryPositivity.RawShuffle.globalStringPBWBasis_weight line 168