OAI/RepresentationTheory/UniversalSquare/Band/OneExtra.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

One Extra.

  1. lemma OAI.Saxl.intertwining_comp_ne_zero line 16
  2. def OAI.Saxl.columnSquareWord line 31
  3. def OAI.Saxl.columnSquareCyclic line 35
  4. def OAI.Saxl.rowColumnTransposeCyclicMap line 38
  5. lemma OAI.Saxl.rowColumnTransposeCyclicMap_injective line 54
  6. theorem OAI.Saxl.sign_rowColumn_support_of_columnSquare line 60
  7. lemma OAI.Saxl.transposeTableau_move line 88
  8. lemma OAI.Saxl.rowColumnWord_move line 93
  9. lemma OAI.Saxl.cyclic_translate_eq line 102
  10. lemma OAI.Saxl.rowColumnCyclic_tableau_independent line 112
  11. theorem OAI.Saxl.rowColumn_support_change_tableau line 117
  12. theorem OAI.Saxl.ShortColumns.even_columnSquare_support line 129
  13. theorem OAI.Saxl.ShortColumns.odd_columnSquare_support line 144
  14. theorem OAI.Saxl.ShortColumns.one_extra_even line 160
  15. theorem OAI.Saxl.ShortColumns.one_extra_odd line 169
  16. def OAI.Saxl.ShortColumns.RowParity line 179
  17. theorem OAI.Saxl.ShortColumns.one_extra line 183