OAI/Combinatorics/Chromatic/Shuffle/GlobalTripleGradeInclusion.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.globalTripleGradeLeft line 14
  2. def OAI.ElementaryPositivity.RawShuffle.globalTripleGradeRight line 25
  3. lemma OAI.ElementaryPositivity.RawShuffle.globalTripleGrade_assoc line 37
  4. lemma OAI.ElementaryPositivity.RawShuffle.globalTripleGrade_left_natural line 52
  5. lemma OAI.ElementaryPositivity.RawShuffle.globalTripleGrade_right_natural line 82
  6. abbrev OAI.ElementaryPositivity.RawShuffle.LeftSlopeTriple line 121
  7. abbrev OAI.ElementaryPositivity.RawShuffle.RightSlopeTriple line 123
  8. abbrev OAI.ElementaryPositivity.RawShuffle.SlopeTriple line 125
  9. def OAI.ElementaryPositivity.RawShuffle.leftTripleView line 130
  10. def OAI.ElementaryPositivity.RawShuffle.rightTripleView line 134
  11. lemma OAI.ElementaryPositivity.RawShuffle.leftTripleView_injective line 140
  12. lemma OAI.ElementaryPositivity.RawShuffle.rightTripleView_injective line 155
  13. lemma OAI.ElementaryPositivity.RawShuffle.leftTripleView_surjective line 167
  14. lemma OAI.ElementaryPositivity.RawShuffle.rightTripleView_surjective line 180
  15. def OAI.ElementaryPositivity.RawShuffle.leftTripleEquiv line 194
  16. def OAI.ElementaryPositivity.RawShuffle.rightTripleEquiv line 198
  17. def OAI.ElementaryPositivity.RawShuffle.leftTripleBuild line 203
  18. def OAI.ElementaryPositivity.RawShuffle.rightTripleBuild line 212
  19. lemma OAI.ElementaryPositivity.RawShuffle.leftTripleView_build line 223
  20. lemma OAI.ElementaryPositivity.RawShuffle.rightTripleView_build line 230
  21. lemma OAI.ElementaryPositivity.RawShuffle.leftTripleBuild_view line 237
  22. lemma OAI.ElementaryPositivity.RawShuffle.rightTripleBuild_view line 243
  23. lemma OAI.ElementaryPositivity.RawShuffle.sum_slopeTriple line 248