OAI/RepresentationTheory/UniversalSquare/Support/AttachmentTransfer.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Attachment Transfer.

  1. def OAI.Saxl.transposeColumnAverage line 16
  2. lemma OAI.Saxl.transposeColumnAverage_nonzero line 22
  3. lemma OAI.Saxl.transposeColumnAverage_fixed line 39
  4. lemma OAI.Saxl.signEquiv_transposeColumnAverage line 50
  5. def OAI.Saxl.rowColumnWord line 72
  6. def OAI.Saxl.rowColumnCyclic line 76
  7. def OAI.Saxl.columnAmbientSignMap line 79
  8. lemma OAI.Saxl.columnAmbientSignMap_subtype line 87
  9. def OAI.Saxl.columnPairAntiMap line 93
  10. lemma OAI.Saxl.columnPairAntiMap_tensor line 102
  11. lemma OAI.Saxl.signed_average_rowColumn line 113
  12. def OAI.Saxl.rowColumnToSquare line 137
  13. theorem OAI.Saxl.polytabloid_square_in_rowColumn_image line 145
  14. theorem OAI.Saxl.subrepresentation_embeds_of_le_range line 168
  15. theorem OAI.Saxl.square_cyclic_embeds_sign_rowColumn line 196