OAI/Combinatorics/Chromatic/Shuffle/HNDetectorBasics.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnKeyLT_irrefl line 11
2. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnKeyLT_trans line 13
3. instance OAI.ElementaryPositivity.SlopeArithmetic.hnKeyLT_strict line 20
4. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnKeyLT_bounds line 23
5. lemma OAI.ElementaryPositivity.SlopeArithmetic.ordered_tail line 26
6. lemma OAI.ElementaryPositivity.SlopeArithmetic.ordered_total_lt_head line 28
7. lemma OAI.ElementaryPositivity.RawShuffle.castS_shuffle_right line 46
8. lemma OAI.ElementaryPositivity.RawShuffle.quotient_clipped_zero line 49
9. def OAI.ElementaryPositivity.RawShuffle.singletonDetector line 54
10. lemma OAI.ElementaryPositivity.RawShuffle.singletonDetector_apply line 57
11. lemma OAI.ElementaryPositivity.RawShuffle.singletonDetector_diagonal line 59
12. lemma OAI.ElementaryPositivity.RawShuffle.singletonDetector_ideal line 72
13. lemma OAI.ElementaryPositivity.RawShuffle.singletonDetector_off line 78
14. structure OAI.ElementaryPositivity.RawShuffle.IsHNDetector line 120
15. def OAI.ElementaryPositivity.RawShuffle.quotientDetector line 129
16. lemma OAI.ElementaryPositivity.RawShuffle.quotientDetector_mk line 133
17. def OAI.ElementaryPositivity.RawShuffle.consDetector line 137
18. lemma OAI.ElementaryPositivity.RawShuffle.consDetector_shuffle line 143
19. lemma OAI.ElementaryPositivity.RawShuffle.consDetector_apply line 152
20. lemma OAI.ElementaryPositivity.RawShuffle.consDetector_ideal line 159
21. lemma OAI.ElementaryPositivity.RawShuffle.consDetector_diagonal line 170
22. lemma OAI.ElementaryPositivity.RawShuffle.consDetector_same_head line 185
23. lemma OAI.ElementaryPositivity.RawShuffle.consDetector_wrong_head line 207
24. theorem OAI.ElementaryPositivity.RawShuffle.hn_detector_exists line 228