OAI/RepresentationTheory/UniversalSquare/Support/PairRun.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.Balance.pairColumns line 15
2. def OAI.Saxl.Balance.pairParts line 18
3. def OAI.Saxl.Balance.pairMarks line 21
4. lemma OAI.Saxl.Balance.pairColumns_succ line 24
5. lemma OAI.Saxl.Balance.pairParts_succ line 28
6. lemma OAI.Saxl.Balance.pairMarks_succ line 32
7. lemma OAI.Saxl.Balance.mem_pairMarks line 36
8. lemma OAI.Saxl.Balance.pairMarks_bound line 41
9. lemma OAI.Saxl.Balance.pairMarks_separated line 46
10. lemma OAI.Saxl.Balance.pairColumns_perm line 52
11. lemma OAI.Saxl.Balance.pairParts_length line 63
12. lemma OAI.Saxl.Balance.pairParts_positive line 68
13. lemma OAI.Saxl.Balance.pairParts_bound line 73
14. theorem OAI.Saxl.Balance.WordPacking.pairRun line 80