OAI/Combinatorics/Chromatic/Shuffle/GlobalHilbertGrading.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.globalOriginalComponent line 16
  2. lemma OAI.ElementaryPositivity.RawShuffle.globalOriginalComponent_lof line 23
  3. lemma OAI.ElementaryPositivity.RawShuffle.globalOriginalComponent_of_mem line 30
  4. lemma OAI.ElementaryPositivity.RawShuffle.unitalOriginalHomogeneous_range line 47
  5. lemma OAI.ElementaryPositivity.RawShuffle.unitalOriginalHomogeneous_finite line 58
  6. lemma OAI.ElementaryPositivity.RawShuffle.globalOriginalComponent_range line 67
  7. lemma OAI.ElementaryPositivity.RawShuffle.globalOriginalComponent_finite line 78
  8. abbrev OAI.ElementaryPositivity.RawShuffle.StringPBWIndex line 94
  9. def OAI.ElementaryPositivity.RawShuffle.stringPBWGrade line 96
  10. abbrev OAI.ElementaryPositivity.RawShuffle.StringPBWGradedIndex line 101
  11. lemma OAI.ElementaryPositivity.RawShuffle.stringPBWBasis_component line 104
  12. def OAI.ElementaryPositivity.RawShuffle.stringPBWGradedBasis line 111
  13. lemma OAI.ElementaryPositivity.RawShuffle.stringPBWGradedIndex_finite line 118
  14. lemma OAI.ElementaryPositivity.RawShuffle.globalOriginalComponent_rank line 123
  15. theorem OAI.ElementaryPositivity.RawShuffle.stringPBWHilbert_coefficient line 130
  16. lemma OAI.ElementaryPositivity.RawShuffle.unitalOriginalNonzero_rank line 148
  17. theorem OAI.ElementaryPositivity.RawShuffle.sourcePBWHilbert_coefficient line 164