OAI/Combinatorics/Chromatic/Shuffle/RawGradedAlgebra.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.rawComponent line 13
  2. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 14) line 14
  3. instance OAI.ElementaryPositivity.RawShuffle.(instance at line 16) line 16
  4. instance OAI.ElementaryPositivity.RawShuffle.rawGradedMul line 19
  5. instance OAI.ElementaryPositivity.RawShuffle.rawGradedOne line 21
  6. lemma OAI.ElementaryPositivity.RawShuffle.castS_heq line 25
  7. lemma OAI.ElementaryPositivity.RawShuffle.raw_one_mul line 29
  8. lemma OAI.ElementaryPositivity.RawShuffle.raw_mul_one line 32
  9. lemma OAI.ElementaryPositivity.RawShuffle.raw_mul_assoc line 35
  10. instance OAI.ElementaryPositivity.RawShuffle.rawGradedMonoid line 38
  11. instance OAI.ElementaryPositivity.RawShuffle.rawGradedRing line 40
  12. lemma OAI.ElementaryPositivity.RawShuffle.raw_smul_mul line 45
  13. lemma OAI.ElementaryPositivity.RawShuffle.raw_mul_smul line 49
  14. instance OAI.ElementaryPositivity.RawShuffle.rawGradedAlgebra line 53
  15. abbrev OAI.ElementaryPositivity.RawShuffle.RawAlgebra line 56
  16. def OAI.ElementaryPositivity.RawShuffle.rawLof line 57
  17. lemma OAI.ElementaryPositivity.RawShuffle.rawLof_mul line 59
  18. lemma OAI.ElementaryPositivity.RawShuffle.rawLof_cast line 63
  19. def OAI.ElementaryPositivity.RawShuffle.rawDimensionSpace line 74
  20. def OAI.ElementaryPositivity.RawShuffle.rawSectionSpace line 76
  21. lemma OAI.ElementaryPositivity.RawShuffle.rawSectionSpace_le line 79
  22. lemma OAI.ElementaryPositivity.RawShuffle.rawDimensionSpace_mul line 83
  23. lemma OAI.ElementaryPositivity.RawShuffle.rawDimensionSpace_zero line 88
  24. lemma OAI.ElementaryPositivity.RawShuffle.rawDimensionSpace_decompose line 97
  25. theorem OAI.ElementaryPositivity.RawShuffle.raw_hn_spanning line 130
  26. def OAI.ElementaryPositivity.RawShuffle.quotientSection line 136
  27. lemma OAI.ElementaryPositivity.RawShuffle.quotientSection_rightInverse line 139
  28. theorem OAI.ElementaryPositivity.RawShuffle.actual_raw_hn_spanning line 146