OAI/Combinatorics/Chromatic/Shuffle/UnitalCoproductUnits.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.unitalSeparationConstant_zero_left line 14
2. lemma OAI.ElementaryPositivity.RawShuffle.unitalSeparationConstant_zero_right line 29
3. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.extendPolynomial_map_algebra line 54
4. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.node_le_iff line 64
5. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.filtrationDimensionEquiv_val line 70
6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.weightComponent_natural line 78
7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.totalLeadingPolynomial_natural line 95
8. def OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.OrderPreserving line 107
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.assoc_orderPreserving line 111
10. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.centerPower_natural line 123
11. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.centerNumerator_natural line 137
12. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.centerDenominator_natural line 143
13. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.clearedLeading_natural line 148
14. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.normalizedSymbol_natural line 165