OAI/RepresentationTheory/UniversalSquare/Balance/BalancedColumns.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Balanced Columns.

  1. def OAI.Saxl.Columns.doubled line 15
  2. lemma OAI.Saxl.Columns.doubled_nil line 17
  3. lemma OAI.Saxl.Columns.doubled_cons line 18
  4. lemma OAI.Saxl.Columns.doubled_map line 21
  5. lemma OAI.Saxl.Columns.doubled_sum line 27
  6. lemma OAI.Saxl.Columns.doubled_countP line 32
  7. lemma OAI.Saxl.Columns.doubled_mem line 38
  8. lemma OAI.Saxl.Columns.doubled_perm line 43
  9. theorem OAI.Saxl.Columns.balanced_heights line 47
  10. lemma OAI.Saxl.Columns.odd_sum_has_odd line 74
  11. theorem OAI.Saxl.Columns.balanced_even_splits line 85
  12. theorem OAI.Saxl.Columns.balanced_double_splits line 103
  13. lemma OAI.Saxl.Columns.columnShape_perm line 181
  14. lemma OAI.Saxl.Columns.count_columns line 190
  15. lemma OAI.Saxl.Columns.columnShape_doubled_halfRows line 194
  16. lemma OAI.Saxl.Columns.columns_bounded line 205
  17. theorem OAI.Saxl.Columns.even_rows_allocation line 211