OAI/Combinatorics/Chromatic/Shuffle/SymmetricSpace.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.symmetricSpace line 12
  2. abbrev OAI.ElementaryPositivity.RawShuffle.S line 20
  3. def OAI.ElementaryPositivity.RawShuffle.shufflePolynomial line 22
  4. lemma OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_eq line 27
  5. lemma OAI.ElementaryPositivity.RawShuffle.rawShuffle_add_left line 32
  6. lemma OAI.ElementaryPositivity.RawShuffle.rawShuffle_add_right line 38
  7. lemma OAI.ElementaryPositivity.RawShuffle.rawShuffle_smul_left line 44
  8. lemma OAI.ElementaryPositivity.RawShuffle.rawShuffle_smul_right line 52
  9. lemma OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_add_left line 60
  10. lemma OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_add_right line 67
  11. lemma OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_smul_left line 74
  12. lemma OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_smul_right line 80
  13. def OAI.ElementaryPositivity.RawShuffle.shuffleLinear line 86
  14. def OAI.ElementaryPositivity.RawShuffle.translation line 102
  15. lemma OAI.ElementaryPositivity.RawShuffle.translation_X line 106
  16. lemma OAI.ElementaryPositivity.RawShuffle.translation_C line 108
  17. lemma OAI.ElementaryPositivity.RawShuffle.translation_rename line 111
  18. lemma OAI.ElementaryPositivity.RawShuffle.translation_add line 117
  19. lemma OAI.ElementaryPositivity.RawShuffle.translation_zero line 123
  20. def OAI.ElementaryPositivity.RawShuffle.translationEquiv line 128
  21. def OAI.ElementaryPositivity.RawShuffle.translationFraction line 134
  22. lemma OAI.ElementaryPositivity.RawShuffle.translationFraction_algebraMap line 140
  23. lemma OAI.ElementaryPositivity.RawShuffle.translation_diagonal line 145
  24. lemma OAI.ElementaryPositivity.RawShuffle.translation_cutFactor line 150
  25. lemma OAI.ElementaryPositivity.RawShuffle.translation_cutDenominator line 155
  26. lemma OAI.ElementaryPositivity.RawShuffle.translation_cutNumerator line 160
  27. lemma OAI.ElementaryPositivity.RawShuffle.translation_rawShuffle line 166
  28. lemma OAI.ElementaryPositivity.RawShuffle.translation_symmetric line 174
  29. def OAI.ElementaryPositivity.RawShuffle.translationS line 180
  30. lemma OAI.ElementaryPositivity.RawShuffle.translation_shufflePolynomial line 185
  31. def OAI.ElementaryPositivity.RawShuffle.dimensionCast line 201
  32. lemma OAI.ElementaryPositivity.RawShuffle.dimensionCast_rfl line 205
  33. lemma OAI.ElementaryPositivity.RawShuffle.translation_dimensionCast line 209
  34. def OAI.ElementaryPositivity.RawShuffle.destabilizingGenerators line 213
  35. def OAI.ElementaryPositivity.RawShuffle.destabilizingSpace line 217
  36. lemma OAI.ElementaryPositivity.RawShuffle.translation_generator line 220
  37. lemma OAI.ElementaryPositivity.RawShuffle.translation_destabilizing line 227
  38. abbrev OAI.ElementaryPositivity.RawShuffle.B line 234
  39. def OAI.ElementaryPositivity.RawShuffle.translationB line 237
  40. lemma OAI.ElementaryPositivity.RawShuffle.translationB_mk line 242
  41. lemma OAI.ElementaryPositivity.RawShuffle.translationS_add line 248
  42. lemma OAI.ElementaryPositivity.RawShuffle.translationS_zero line 254
  43. lemma OAI.ElementaryPositivity.RawShuffle.translationB_add line 258
  44. lemma OAI.ElementaryPositivity.RawShuffle.translationB_zero line 264
  45. def OAI.ElementaryPositivity.RawShuffle.translationBEquiv line 269