OAI/Combinatorics/Chromatic/Shuffle/NormalizedTripleSymbol.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.SplitTree.tripleClearedLeading line 12
2. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.denominator_tripleClearedLeading line 20
3. def OAI.ElementaryPositivity.RawShuffle.SplitTree.tripleClearedLeadingMap line 31
4. def OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTripleSymbol line 51
5. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTripleSymbol_tmul line 60
6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTripleSymbol_eq_zero_iff line 88
7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.degreeCut_node_tmul line 111
8. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.refinedTripleCenterPolynomial_coeff_degreeCut line 123
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTripleSymbol_next_zero line 152
10. theorem OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTripleSymbol_detect line 165