OAI/Combinatorics/Chromatic/Shuffle/NormalizedTensorSymbol.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.internalDenominator_ne_zero line 17
2. def OAI.ElementaryPositivity.RawShuffle.SplitTree.tensorClearedLeading line 23
3. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.denominator_tensorClearedLeading line 31
4. def OAI.ElementaryPositivity.RawShuffle.SplitTree.tensorClearedLeadingMap line 42
5. def OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTensorSymbol line 62
6. theorem OAI.ElementaryPositivity.RawShuffle.SplitTree.coproduct_normalized_symbol line 71
7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.internalNumerator_ne_zero line 123
8. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTensorSymbol_tmul line 129
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTensorSymbol_eq_zero_iff line 157
10. theorem OAI.ElementaryPositivity.RawShuffle.SplitTree.normalizedTensorSymbol_detect line 171