OAI/Probability/BinarySweep/YoungTheory/HookCut.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Young.hookPart line 16
  2. def OAI.BinaryCoordinateSweeps.Young.shiftCell line 27
  3. lemma OAI.BinaryCoordinateSweeps.Young.shiftCell_injective line 29
  4. def OAI.BinaryCoordinateSweeps.Young.southeast line 35
  5. lemma OAI.BinaryCoordinateSweeps.Young.mem_hookPart line 43
  6. lemma OAI.BinaryCoordinateSweeps.Young.mem_southeast line 49
  7. lemma OAI.BinaryCoordinateSweeps.Young.hookPart_inHook line 54
  8. def OAI.BinaryCoordinateSweeps.Young.hookIn line 58
  9. def OAI.BinaryCoordinateSweeps.Young.southeastIn line 62
  10. lemma OAI.BinaryCoordinateSweeps.Young.row_hookIn line 66
  11. lemma OAI.BinaryCoordinateSweeps.Young.col_hookIn line 67
  12. lemma OAI.BinaryCoordinateSweeps.Young.row_southeastIn line 68
  13. lemma OAI.BinaryCoordinateSweeps.Young.col_southeastIn line 69
  14. def OAI.BinaryCoordinateSweeps.Young.cutEquiv line 71
  15. lemma OAI.BinaryCoordinateSweeps.Young.cutEquiv_inl line 110
  16. lemma OAI.BinaryCoordinateSweeps.Young.cutEquiv_inr line 112
  17. lemma OAI.BinaryCoordinateSweeps.Young.card_cut line 115
  18. def OAI.BinaryCoordinateSweeps.Young.cutPerm line 130
  19. lemma OAI.BinaryCoordinateSweeps.Young.cutPerm_apply_hook line 133
  20. lemma OAI.BinaryCoordinateSweeps.Young.cutPerm_apply_southeast line 140
  21. lemma OAI.BinaryCoordinateSweeps.Young.cutPerm_injective line 147
  22. lemma OAI.BinaryCoordinateSweeps.Young.signC_cutPerm line 150
  23. def OAI.BinaryCoordinateSweeps.Young.glueLabels line 156
  24. lemma OAI.BinaryCoordinateSweeps.Young.glueLabels_hook line 159
  25. lemma OAI.BinaryCoordinateSweeps.Young.glueLabels_southeast line 165
  26. lemma OAI.BinaryCoordinateSweeps.Young.labels_cutPerm line 171
  27. def OAI.BinaryCoordinateSweeps.Young.glueTabloid line 184
  28. lemma OAI.BinaryCoordinateSweeps.Young.glueTabloid_val line 191
  29. lemma OAI.BinaryCoordinateSweeps.Young.glueTabloid_injective line 194
  30. lemma OAI.BinaryCoordinateSweeps.Young.glueTabloid_perm line 206
  31. lemma OAI.BinaryCoordinateSweeps.Young.glueTabloid_smul line 212