OAI/Combinatorics/Chromatic/Shuffle/DimensionEquivS.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.SplitTree.dimensionEquivS line 13
2. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.dimensionEquivS_val line 18
3. def OAI.ElementaryPositivity.RawShuffle.SplitTree.Vars line 25
4. def OAI.ElementaryPositivity.RawShuffle.SplitTree.varEquiv line 29
5. def OAI.ElementaryPositivity.RawShuffle.SplitTree.tensorValue line 34
6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.tensorValue_tmul line 40
7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.tensorValue_injective line 46
8. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.tensorValue_rawRestriction line 54
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.rawRestriction_regroup line 76
10. def OAI.ElementaryPositivity.RawShuffle.SplitTree.packFiberEquiv line 90
11. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.pack_equiv_eq_packAction line 102
12. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.rename_pack_preserving line 116
13. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.rawRestriction_regroup_permuted line 121
14. def OAI.ElementaryPositivity.RawShuffle.SplitTree.packIndex line 138
15. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.varEquiv_fst line 144
16. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.varEquiv_symm_packIndex line 153
17. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.rawRestriction_regroup_of_pack_preserving line 157