OAI/Combinatorics/Chromatic/Histories/TwoLeafDiagonal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.CenterCalculus.ofTwo line 11
2. lemma OAI.ElementaryPositivity.CenterCalculus.ofTwo_C line 14
3. lemma OAI.ElementaryPositivity.CenterCalculus.ofTwo_X line 17
4. lemma OAI.ElementaryPositivity.CenterCalculus.evalRat_ofTwo line 22
5. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centeredRestrictionB_two_eval line 42
6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.twoLeading_eq line 56
7. theorem OAI.ElementaryPositivity.RawShuffle.SplitTree.twoLeading_diagonal_divisible line 74
8. def OAI.ElementaryPositivity.RawShuffle.SplitTree.leafDimension line 102
9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.leafDimension line 109
10. def OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.assocInv line 120
11. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.assocInv_centers_left line 127
12. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.assocInv_centers_mid line 130
13. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.isolate_one line 133
14. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.Regroup.isolate_pair line 164