OAI/Combinatorics/Chromatic/Shuffle/ComponentB.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.componentB line 12
  2. lemma OAI.ElementaryPositivity.RawShuffle.componentB_mk line 17
  3. lemma OAI.ElementaryPositivity.RawShuffle.componentS_componentS line 23
  4. lemma OAI.ElementaryPositivity.RawShuffle.componentB_componentB line 27
  5. lemma OAI.ElementaryPositivity.RawShuffle.componentB_idempotent line 38
  6. lemma OAI.ElementaryPositivity.RawShuffle.componentB_negative line 43
  7. theorem OAI.ElementaryPositivity.RawShuffle.componentB_finite_decomposition line 52
  8. def OAI.ElementaryPositivity.RawShuffle.gradeB line 72
  9. lemma OAI.ElementaryPositivity.RawShuffle.mem_gradeB_iff line 75
  10. lemma OAI.ElementaryPositivity.RawShuffle.componentB_on_grade line 84
  11. theorem OAI.ElementaryPositivity.RawShuffle.gradeB_finite_independent line 90
  12. lemma OAI.ElementaryPositivity.RawShuffle.dimensionCast_trans line 114
  13. lemma OAI.ElementaryPositivity.RawShuffle.shuffle_assoc_cast line 118
  14. lemma OAI.ElementaryPositivity.RawShuffle.shuffle_assoc_cast_symm line 125
  15. lemma OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_zero_left line 132
  16. lemma OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_zero_right line 135
  17. lemma OAI.ElementaryPositivity.RawShuffle.destabilizing_shuffle_left line 138
  18. lemma OAI.ElementaryPositivity.RawShuffle.destabilizing_shuffle_right line 159
  19. def OAI.ElementaryPositivity.RawShuffle.shuffleB line 181
  20. lemma OAI.ElementaryPositivity.RawShuffle.shuffleB_mk line 212