OAI/RepresentationTheory/UniversalSquare/Balance/BalanceProduct.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Balance Product.

  1. def OAI.Saxl.Balance.cyclicSquareMap line 18
  2. lemma OAI.Saxl.Balance.cyclicSquareMap_tmul line 29
  3. theorem OAI.Saxl.Balance.product_mem_square line 33
  4. def OAI.Saxl.Balance.joinedLabels line 56
  5. lemma OAI.Saxl.Balance.joinedLabels_left line 59
  6. lemma OAI.Saxl.Balance.joinedLabels_right line 63
  7. def OAI.Saxl.Balance.joinedFiberHom line 67
  8. lemma OAI.Saxl.Balance.joinedFiberHom_surjective line 79
  9. lemma OAI.Saxl.Balance.componentWords_joined line 109
  10. lemma OAI.Saxl.Balance.component_projection_product line 131
  11. lemma OAI.Saxl.Balance.joined_component_sum line 142
  12. lemma OAI.Saxl.Balance.product_fixed_sums line 153
  13. def OAI.Saxl.Balance.outerWordMap line 162
  14. lemma OAI.Saxl.Balance.outerWordMap_injective line 180