OAI/Combinatorics/Chromatic/Walls/TriangularGaps.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ElementaryPositivity.TriangularGaps.Recurrence line 8
2. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.diagonal_all line 25
3. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.row_mono_add line 32
4. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.row_le_start line 43
5. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.partial_total line 48
6. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.total_le_one line 66
7. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.unique_start line 71
8. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.anchor_run line 103
9. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.other_rows_zero line 115
10. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.diagonal_sum line 124
11. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.u_one_row line 134
12. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.row_formula line 154
13. lemma OAI.ElementaryPositivity.TriangularGaps.Recurrence.xi_zero_before line 164
14. theorem OAI.ElementaryPositivity.TriangularGaps.Recurrence.positive_gap_zero_pairings line 183
15. structure OAI.ElementaryPositivity.TriangularGaps.IntegerGaps line 216
16. def OAI.ElementaryPositivity.TriangularGaps.IntegerGaps.t line 230
17. lemma OAI.ElementaryPositivity.TriangularGaps.IntegerGaps.t_row line 232
18. lemma OAI.ElementaryPositivity.TriangularGaps.IntegerGaps.t_start line 240
19. lemma OAI.ElementaryPositivity.TriangularGaps.IntegerGaps.t_nonneg line 247
20. def OAI.ElementaryPositivity.TriangularGaps.IntegerGaps.recurrence line 258
21. theorem OAI.ElementaryPositivity.TriangularGaps.IntegerGaps.positive_gap_zero_pairings line 280