OAI/Combinatorics/Chromatic/Shuffle/HNIndependent.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.hnPolynomialExpansion line 15
  2. lemma OAI.ElementaryPositivity.RawShuffle.hnExpansionRaw_polynomial line 19
  3. instance OAI.ElementaryPositivity.RawShuffle.hnIndex_strict line 28
  4. theorem OAI.ElementaryPositivity.RawShuffle.hnPolynomialExpansion_injective line 33
  5. lemma OAI.ElementaryPositivity.RawShuffle.hnPolynomialExpansion_surjective line 52
  6. def OAI.ElementaryPositivity.RawShuffle.hnOrderedEquiv line 62
  7. def OAI.ElementaryPositivity.RawShuffle.degreeQuotient line 77
  8. lemma OAI.ElementaryPositivity.RawShuffle.degreeQuotient_surjective line 82
  9. def OAI.ElementaryPositivity.RawShuffle.degreeSection line 92
  10. lemma OAI.ElementaryPositivity.RawShuffle.degreeSection_rightInverse line 96
  11. def OAI.ElementaryPositivity.RawShuffle.gradeBEquiv line 101
  12. lemma OAI.ElementaryPositivity.RawShuffle.gradeBEquiv_of line 103
  13. lemma OAI.ElementaryPositivity.RawShuffle.gradeBEquiv_symm_homogeneous line 106
  14. def OAI.ElementaryPositivity.RawShuffle.homogeneousSection line 111
  15. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousSection_on_grade line 114
  16. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousSection_rightInverse line 119
  17. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousSection_graded line 135