OAI/Combinatorics/Chromatic/Shuffle/SymbolDetection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.SlopeEulerSymmetric line 13
2. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.leafDimension_onSlope line 19
3. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.pairSymmetric_of_slope line 30
4. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.totalLeadingPolynomial_next_zero line 38
5. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.totalLeadingPolynomial_zero_test line 53
6. structure OAI.ElementaryPositivity.RawShuffle.SymbolIndex line 65
7. def OAI.ElementaryPositivity.RawShuffle.filtrationDimensionEquiv line 71
8. def OAI.ElementaryPositivity.RawShuffle.indexedSymbol line 77
9. def OAI.ElementaryPositivity.RawShuffle.symbolFamily line 86
10. lemma OAI.ElementaryPositivity.RawShuffle.symbolFamily_ker line 93
11. def OAI.ElementaryPositivity.RawShuffle.gradeSymbolFamily line 116
12. theorem OAI.ElementaryPositivity.RawShuffle.gradeSymbolFamily_injective line 124