OAI/Combinatorics/Chromatic/Shuffle/TensorColumnSeriesFiltration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.TensorColumns.seriesProduct line 17
2. lemma OAI.ElementaryPositivity.TensorColumns.seriesProduct_coeff_filtration line 22
3. lemma OAI.ElementaryPositivity.TensorColumns.seriesProduct_constant_filtration line 39
4. def OAI.ElementaryPositivity.RawShuffle.fourInputSeriesB line 78
5. lemma OAI.ElementaryPositivity.RawShuffle.fourInputSeriesB_constant_next line 90
6. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.unitalRestrictionRelativeB_mk line 135
7. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.unitalSeparationSeries_mk line 143