OAI/Combinatorics/Chromatic/Shuffle/Regroup.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup line 14
2. def OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.vars line 22
3. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.pack line 30
4. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.dimension line 42
5. def OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.equivalence line 50
6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.tensorMap_natural line 59
7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.tensorValue_natural line 90
8. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.rawRestriction_natural line 128
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.dimensionEquivB_mk line 135
10. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.restrictionB_natural line 142