OAI/Combinatorics/Chromatic/Shuffle/PrimitiveOperators.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.derivativeB_properFiltered line 12
2. lemma OAI.ElementaryPositivity.RawShuffle.meanMultiplyB_properFiltered line 21
3. lemma OAI.ElementaryPositivity.RawShuffle.gradeDerivative_primitive line 29
4. lemma OAI.ElementaryPositivity.RawShuffle.gradeMeanMultiply_primitive line 43
5. lemma OAI.ElementaryPositivity.RawShuffle.gradeDerivative_locally_nilpotent line 57
6. def OAI.ElementaryPositivity.RawShuffle.primitiveDerivative line 63
7. def OAI.ElementaryPositivity.RawShuffle.primitiveMeanMultiply line 69
8. lemma OAI.ElementaryPositivity.RawShuffle.primitive_weyl line 75
9. lemma OAI.ElementaryPositivity.RawShuffle.primitiveDerivative_locally_nilpotent line 83
10. def OAI.ElementaryPositivity.RawShuffle.primitiveStringDecomposition line 92