OAI/RepresentationTheory/UniversalSquare/Balance/BalanceColumns.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Balance Columns.

  1. def OAI.Saxl.Balance.fixedSumSpace line 17
  2. lemma OAI.Saxl.Balance.component_sum_perm line 30
  3. lemma OAI.Saxl.Balance.fixedSumSpace_invariant line 38
  4. def OAI.Saxl.Balance.columnRowSums line 46
  5. def OAI.Saxl.Balance.localColumnSub line 50
  6. lemma OAI.Saxl.Balance.localColumnSub_mem_specht line 53
  7. lemma OAI.Saxl.Balance.polytabloid_fixed_column_sums line 67
  8. lemma OAI.Saxl.Balance.localColumnSub_fixed_sums line 89
  9. def OAI.Saxl.Balance.localColumnTensorMap line 106
  10. lemma OAI.Saxl.Balance.localColumnTensorMap_tmul line 124
  11. lemma OAI.Saxl.Balance.localColumnTensorMap_mem line 129
  12. def OAI.Saxl.Balance.columnOutputSums line 142
  13. theorem OAI.Saxl.Balance.localColumnTensorMap_fixed_sums line 146
  14. lemma OAI.Saxl.Balance.componentWords_invariant_fiber line 172
  15. def OAI.Saxl.Balance.componentProjection line 187
  16. def OAI.Saxl.Balance.projectedColumnSquare line 202
  17. def OAI.Saxl.Balance.rangeQuotient line 208
  18. lemma OAI.Saxl.Balance.rangeQuotient_surjective line 220
  19. theorem OAI.Saxl.Balance.projected_range_support line 227
  20. theorem OAI.Saxl.Balance.projected_columns_support line 264
  21. theorem OAI.Saxl.Balance.kronecker_pos_of_projected_columns line 294