OAI/Combinatorics/Chromatic/Shuffle/GlobalPrimitiveLog.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.signedLeftRight_convolution line 15
2. lemma OAI.ElementaryPositivity.RawShuffle.signedRightLeft_convolution line 24
3. lemma OAI.ElementaryPositivity.RawShuffle.convPost_id line 34
4. lemma OAI.ElementaryPositivity.RawShuffle.convPost_J line 38
5. lemma OAI.ElementaryPositivity.RawShuffle.convVanishes_post line 43
6. lemma OAI.ElementaryPositivity.RawShuffle.signedConvolution_J_product line 49
7. lemma OAI.ElementaryPositivity.RawShuffle.signedConvolution_J_commute line 58
8. def OAI.ElementaryPositivity.RawShuffle.globalPrimitiveLog line 66
9. theorem OAI.ElementaryPositivity.RawShuffle.globalPrimitiveLog_primitive line 69