OAI/Combinatorics/Chromatic/Shuffle/GlobalLocalPrimitives.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.globalPrimitive_iff_local line 18
  2. lemma OAI.ElementaryPositivity.RawShuffle.derivativeS_component line 67
  3. lemma OAI.ElementaryPositivity.RawShuffle.derivativeB_component line 83
  4. lemma OAI.ElementaryPositivity.RawShuffle.meanS_homogeneous line 95
  5. lemma OAI.ElementaryPositivity.RawShuffle.componentS_mean line 102
  6. lemma OAI.ElementaryPositivity.RawShuffle.meanMultiplyB_component line 109
  7. lemma OAI.ElementaryPositivity.RawShuffle.gradeDerivative_component line 120
  8. lemma OAI.ElementaryPositivity.RawShuffle.gradeMeanMultiply_component line 129
  9. def OAI.ElementaryPositivity.RawShuffle.primitiveComponent line 153
  10. lemma OAI.ElementaryPositivity.RawShuffle.primitiveDerivative_component line 158
  11. lemma OAI.ElementaryPositivity.RawShuffle.primitiveMeanMultiply_component line 163
  12. lemma OAI.ElementaryPositivity.RawShuffle.primitiveComponent_ker line 168
  13. def OAI.ElementaryPositivity.RawShuffle.stringBaseComponent line 174
  14. lemma OAI.ElementaryPositivity.RawShuffle.stringBaseComponent_twice line 179
  15. def OAI.ElementaryPositivity.RawShuffle.homogeneousStringBases line 189
  16. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousStringBases_span line 192
  17. def OAI.ElementaryPositivity.RawShuffle.StringBaseIndex line 206
  18. def OAI.ElementaryPositivity.RawShuffle.homogeneousStringBaseBasis line 210
  19. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousStringBaseBasis_exists_degree line 215
  20. def OAI.ElementaryPositivity.RawShuffle.stringBaseDegree line 220
  21. lemma OAI.ElementaryPositivity.RawShuffle.stringBaseDegree_spec line 223
  22. lemma OAI.ElementaryPositivity.RawShuffle.stringBaseDegree_nonneg line 229
  23. lemma OAI.ElementaryPositivity.RawShuffle.primitiveMeanMultiply_pow_component line 238
  24. def OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveStringBasis line 247
  25. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveStringBasis_apply line 253
  26. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousPrimitiveStringBasis_degree line 260