OAI/Probability/BinarySweep/YoungTheory/HookWord.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Young.InHook line 15
  2. def OAI.BinaryCoordinateSweeps.Young.hookLabel line 20
  3. lemma OAI.BinaryCoordinateSweeps.Young.hookLabel_top line 24
  4. lemma OAI.BinaryCoordinateSweeps.Young.hookLabel_bottom line 29
  5. lemma OAI.BinaryCoordinateSweeps.Young.hookLabel_eq_top line 34
  6. lemma OAI.BinaryCoordinateSweeps.Young.hookLabel_eq_bottom line 41
  7. lemma OAI.BinaryCoordinateSweeps.Young.hook_return_column_fixes line 48
  8. lemma OAI.BinaryCoordinateSweeps.Young.hook_return_row_fixes line 60
  9. def OAI.BinaryCoordinateSweeps.Young.hookWord line 72
  10. lemma OAI.BinaryCoordinateSweeps.Young.hookWord_comp_eq line 75
  11. lemma OAI.BinaryCoordinateSweeps.Young.hook_return_sign line 88
  12. instance OAI.BinaryCoordinateSweeps.Young.rowStabilizer_fintype line 138
  13. def OAI.BinaryCoordinateSweeps.Young.hookRep line 140
  14. def OAI.BinaryCoordinateSweeps.Young.hookRowVector line 144
  15. lemma OAI.BinaryCoordinateSweeps.Young.hookRowVector_fixed line 148
  16. def OAI.BinaryCoordinateSweeps.Young.hookMap line 155
  17. lemma OAI.BinaryCoordinateSweeps.Young.hookMap_poly line 164
  18. lemma OAI.BinaryCoordinateSweeps.Young.hook_term_coefficient line 180
  19. lemma OAI.BinaryCoordinateSweeps.Young.hookMap_poly_coefficient line 192
  20. lemma OAI.BinaryCoordinateSweeps.Young.hookMap_nonzero line 199
  21. theorem OAI.BinaryCoordinateSweeps.Young.hookMap_injective line 227