OAI/RepresentationTheory/UniversalSquare/Specht/ShortColumns.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Short Columns.

  1. def OAI.Saxl.ShortColumns.shape line 16
  2. lemma OAI.Saxl.ShortColumns.mem_shape line 19
  3. lemma OAI.Saxl.ShortColumns.height_le line 28
  4. def OAI.Saxl.ShortColumns.oddTableau line 34
  5. lemma OAI.Saxl.ShortColumns.oddTableau_row line 72
  6. lemma OAI.Saxl.ShortColumns.oddTableau_col_iff line 77
  7. lemma OAI.Saxl.ShortColumns.oddTableau_group line 85
  8. lemma OAI.Saxl.ShortColumns.oddTableau_polytabloid line 93
  9. def OAI.Saxl.ShortColumns.oddSplit line 102
  10. lemma OAI.Saxl.ShortColumns.oddSplit_left line 107
  11. lemma OAI.Saxl.ShortColumns.oddSplit_right line 112
  12. def OAI.Saxl.ShortColumns.pairSplit line 115
  13. lemma OAI.Saxl.ShortColumns.pairSplit_left line 131
  14. lemma OAI.Saxl.ShortColumns.pairSplit_right line 134
  15. lemma OAI.Saxl.ShortColumns.shortPairForm_eq line 137
  16. lemma OAI.Saxl.ShortColumns.singleton_square line 143
  17. lemma OAI.Saxl.ShortColumns.odd_square line 150
  18. def OAI.Saxl.ShortColumns.evenTableau line 172
  19. def OAI.Saxl.ShortColumns.evenAlt line 187
  20. lemma OAI.Saxl.ShortColumns.evenTableau_polytabloid line 191
  21. def OAI.Saxl.ShortColumns.appendEven line 196
  22. lemma OAI.Saxl.ShortColumns.appendEven_left line 199
  23. lemma OAI.Saxl.ShortColumns.appendEven_right line 201
  24. lemma OAI.Saxl.ShortColumns.evenAlt_step line 204
  25. lemma OAI.Saxl.ShortColumns.evenAlt_zero line 242
  26. lemma OAI.Saxl.ShortColumns.evenAlt_formula line 258
  27. lemma OAI.Saxl.ShortColumns.even_square line 270