OAI/Combinatorics/Chromatic/Shuffle/GradedCoproduct.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.nextTensorFiltration line 14
2. abbrev OAI.ElementaryPositivity.RawShuffle.SourceTensorAssociatedGrade line 20
3. def OAI.ElementaryPositivity.RawShuffle.separationCoefficientRestricted line 25
4. def OAI.ElementaryPositivity.RawShuffle.gradeSeparationCoefficient line 34
5. lemma OAI.ElementaryPositivity.RawShuffle.gradeSeparationCoefficient_mk line 47
6. theorem OAI.ElementaryPositivity.RawShuffle.gradeSeparationCoefficient_negative line 56
7. def OAI.ElementaryPositivity.RawShuffle.separationCoproduct line 63
8. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.proper line 82
9. lemma OAI.ElementaryPositivity.RawShuffle.properSourceFiltration_allTrees line 91
10. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.totalLeadingPolynomial_proper_next_zero line 105
11. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.tensorTest_next_zero line 119
12. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTensorSymbol_next_zero line 138
13. lemma OAI.ElementaryPositivity.RawShuffle.separationCoproduct_mk_eq_zero_iff line 162
14. lemma OAI.ElementaryPositivity.RawShuffle.separationCoproduct_primitive_zero line 170
15. theorem OAI.ElementaryPositivity.RawShuffle.primitiveSpace_iff_coproducts_zero line 189