OAI/RepresentationTheory/UniversalSquare/Balance/BalanceProjection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Balance Projection.

  1. def OAI.Saxl.Balance.FixedComponentSums line 15
  2. def OAI.Saxl.Balance.balanceWords line 19
  3. def OAI.Saxl.Balance.componentWords line 27
  4. lemma OAI.Saxl.Balance.perm_filter_card line 31
  5. lemma OAI.Saxl.Balance.perm_filter_sum line 45
  6. lemma OAI.Saxl.Balance.balanceWords_invariant line 52
  7. lemma OAI.Saxl.Balance.balanceWords_iff_components line 67
  8. theorem OAI.Saxl.Balance.balance_projection_eq line 86
  9. theorem OAI.Saxl.Balance.component_projection_mem line 99
  10. theorem OAI.Saxl.Balance.components_support_transfer line 110
  11. theorem OAI.Saxl.Balance.balance_support_transfer line 162