OAI/Combinatorics/Chromatic/Shuffle/ShuffleUnits.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.labeledValue_unit line 14
2. def OAI.ElementaryPositivity.RawShuffle.emptyLeftCut line 25
3. def OAI.ElementaryPositivity.RawShuffle.emptyRightCut line 28
4. lemma OAI.ElementaryPositivity.RawShuffle.eq_emptyLeftCut line 32
5. lemma OAI.ElementaryPositivity.RawShuffle.eq_emptyRightCut line 44
6. lemma OAI.ElementaryPositivity.RawShuffle.shuffle_labeled_unit_left line 55
7. lemma OAI.ElementaryPositivity.RawShuffle.shuffle_labeled_unit_right line 71
8. lemma OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_unit_left line 87
9. lemma OAI.ElementaryPositivity.RawShuffle.shufflePolynomial_unit_right line 97
10. lemma OAI.ElementaryPositivity.RawShuffle.S_zero_eq_scalar line 117
11. lemma OAI.ElementaryPositivity.RawShuffle.destabilizingSpace_zero line 124
12. lemma OAI.ElementaryPositivity.RawShuffle.castS_mem_destabilizing line 131
13. lemma OAI.ElementaryPositivity.RawShuffle.destabilizing_shuffle_unit_left line 137
14. lemma OAI.ElementaryPositivity.RawShuffle.destabilizing_shuffle_unit_right line 150
15. def OAI.ElementaryPositivity.RawShuffle.shuffleBUnit line 163
16. lemma OAI.ElementaryPositivity.RawShuffle.shuffleBUnit_mk line 194
17. lemma OAI.ElementaryPositivity.RawShuffle.shuffleBUnit_eq_shuffleB line 200