OAI/RepresentationTheory/UniversalSquare/Specht/RepeatedColumns.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Repeated Columns.

  1. lemma OAI.Saxl.paired_relation_iff_free line 15
  2. lemma OAI.Saxl.paired_term_projection_free line 34
  3. theorem OAI.Saxl.repeated_alt_projection_free line 86
  4. def OAI.Saxl.columnReversalCell line 108
  5. lemma OAI.Saxl.columnReversalCell_involutive line 114
  6. def OAI.Saxl.columnReversalEquiv line 124
  7. def OAI.Saxl.columnReversal line 128
  8. def OAI.Saxl.columnLengthWord line 134
  9. lemma OAI.Saxl.columnLengthWord_fixed line 142
  10. lemma OAI.Saxl.rowWord_column_free line 148
  11. lemma OAI.Saxl.columnReversal_complement line 157
  12. theorem OAI.Saxl.squared_polytabloid_projection line 169
  13. lemma OAI.Saxl.column_projection_coefficient_ne_zero line 180
  14. theorem OAI.Saxl.specht_map_back_of_nonzero line 189
  15. theorem OAI.Saxl.kronecker_pos_of_column_content line 209
  16. lemma OAI.Saxl.tableau_count line 244