OAI/Combinatorics/Chromatic/Shuffle/QuotientAlg.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ElementaryPositivity.RawShuffle.quotientCommRing line 14
  2. instance OAI.ElementaryPositivity.RawShuffle.quotientAlgebra line 16
  3. def OAI.ElementaryPositivity.RawShuffle.quotientAlg line 19
  4. lemma OAI.ElementaryPositivity.RawShuffle.quotientAlg_apply line 22
  5. def OAI.ElementaryPositivity.RawShuffle.tensorValueAlg line 25
  6. lemma OAI.ElementaryPositivity.RawShuffle.tensorValueAlg_apply line 31
  7. lemma OAI.ElementaryPositivity.RawShuffle.tensorValue_mul line 35
  8. def OAI.ElementaryPositivity.RawShuffle.restrictTensorAlg line 39
  9. lemma OAI.ElementaryPositivity.RawShuffle.taylorS_exists line 61
  10. def OAI.ElementaryPositivity.RawShuffle.taylorSValue line 74
  11. lemma OAI.ElementaryPositivity.RawShuffle.map_taylorSValue line 78
  12. lemma OAI.ElementaryPositivity.RawShuffle.polynomial_symmetric_injective line 83
  13. def OAI.ElementaryPositivity.RawShuffle.taylorS line 87
  14. lemma OAI.ElementaryPositivity.RawShuffle.map_taylorS line 125
  15. lemma OAI.ElementaryPositivity.RawShuffle.taylorS_eval line 130
  16. lemma OAI.ElementaryPositivity.RawShuffle.taylorS_coeff_destabilizing line 152
  17. def OAI.ElementaryPositivity.RawShuffle.taylorB line 160
  18. lemma OAI.ElementaryPositivity.RawShuffle.taylorB_mk line 171
  19. lemma OAI.ElementaryPositivity.RawShuffle.eval_map_rat line 174
  20. def OAI.ElementaryPositivity.RawShuffle.relativeTaylor line 184
  21. lemma OAI.ElementaryPositivity.RawShuffle.relativeTaylor_tmul line 193
  22. def OAI.ElementaryPositivity.RawShuffle.quotientTensor line 200
  23. def OAI.ElementaryPositivity.RawShuffle.restrictRelative line 204
  24. lemma OAI.ElementaryPositivity.RawShuffle.relativeTaylor_eval line 211
  25. lemma OAI.ElementaryPositivity.RawShuffle.restrictRelative_eval line 221