OAI/Combinatorics/Chromatic/Shuffle/GlobalPrimitiveGeneration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.convSeries_exp_log line 17
2. theorem OAI.ElementaryPositivity.RawShuffle.globalPrimitiveLog_exponential line 27
3. lemma OAI.ElementaryPositivity.RawShuffle.convolution_mapsTo_mul line 35
4. lemma OAI.ElementaryPositivity.RawShuffle.convolution_mapsTo_pow line 48
5. theorem OAI.ElementaryPositivity.RawShuffle.globalPrimitiveLog_adjoin line 57
6. def OAI.ElementaryPositivity.RawShuffle.globalHomogeneous line 90
7. def OAI.ElementaryPositivity.RawShuffle.convPreservesWeight line 93
8. lemma OAI.ElementaryPositivity.RawShuffle.globalHomogeneous_mul line 97
9. lemma OAI.ElementaryPositivity.RawShuffle.convPreservesWeight_one line 104
10. lemma OAI.ElementaryPositivity.RawShuffle.convPreservesWeight_id line 117
11. lemma OAI.ElementaryPositivity.RawShuffle.convPreservesWeight_sub line 121
12. lemma OAI.ElementaryPositivity.RawShuffle.globalTensorGrade_map_homogeneous line 127
13. lemma OAI.ElementaryPositivity.RawShuffle.convPreservesWeight_mul line 143
14. lemma OAI.ElementaryPositivity.RawShuffle.convPreservesWeight_pow line 165
15. lemma OAI.ElementaryPositivity.RawShuffle.globalPrimitiveLog_homogeneous line 173