OAI/Combinatorics/Chromatic/Shuffle/GlobalSeriesEvaluation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.convSeries_eventually_finite line 16
2. def OAI.ElementaryPositivity.RawShuffle.globalPrimitives line 54
3. lemma OAI.ElementaryPositivity.RawShuffle.mem_globalPrimitives line 61
4. lemma OAI.ElementaryPositivity.RawShuffle.globalPrimitive_counit line 68
5. lemma OAI.ElementaryPositivity.RawShuffle.convVanishes_unit line 81
6. lemma OAI.ElementaryPositivity.RawShuffle.convolution_mul_primitive line 86
7. lemma OAI.ElementaryPositivity.RawShuffle.convolution_pow_primitive line 97
8. lemma OAI.ElementaryPositivity.RawShuffle.convolutionJ_primitive line 109
9. lemma OAI.ElementaryPositivity.RawShuffle.globalPrimitiveLog_homogeneous_primitive line 115
10. theorem OAI.ElementaryPositivity.RawShuffle.globalPrimitiveLog_on_primitive line 139
11. theorem OAI.ElementaryPositivity.RawShuffle.globalPrimitiveLog_range line 155
12. theorem OAI.ElementaryPositivity.RawShuffle.globalPrimitiveLog_idempotent line 163