OAI/Probability/BinarySweep/YoungTheory/CutBranching.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryCoordinateSweeps.Young.CutGroup line 36
  2. def OAI.BinaryCoordinateSweeps.Young.cutSpechtRep line 38
  3. lemma OAI.BinaryCoordinateSweeps.Young.cutSpechtRep_tmul line 42
  4. def OAI.BinaryCoordinateSweeps.Young.cutTabloidRep line 47
  5. lemma OAI.BinaryCoordinateSweeps.Young.cutRestriction_rep line 55
  6. lemma OAI.BinaryCoordinateSweeps.Young.cutTensorInclude_rep line 64
  7. def OAI.BinaryCoordinateSweeps.Young.cutRestrictionIntertwiner line 74
  8. def OAI.BinaryCoordinateSweeps.Young.cutTensorIntertwiner line 79
  9. theorem OAI.BinaryCoordinateSweeps.Young.hook_removal_embedding line 83
  10. def OAI.BinaryCoordinateSweeps.Young.hookPerm line 93
  11. def OAI.BinaryCoordinateSweeps.Young.hookRestriction line 96
  12. def OAI.BinaryCoordinateSweeps.Young.cutSlice line 99
  13. def OAI.BinaryCoordinateSweeps.Young.cutSliceMap line 112
  14. lemma OAI.BinaryCoordinateSweeps.Young.cutSliceMap_injective line 119
  15. theorem OAI.BinaryCoordinateSweeps.Young.hook_removal_multiplicity line 131
  16. abbrev OAI.BinaryCoordinateSweeps.Young.HookInducedSpace line 145
  17. def OAI.BinaryCoordinateSweeps.Young.hookInducedRep line 147
  18. lemma OAI.BinaryCoordinateSweeps.Young.hookPerm_block line 150
  19. theorem OAI.BinaryCoordinateSweeps.Young.hook_induced_multiplicity line 152
  20. lemma OAI.BinaryCoordinateSweeps.Young.hook_induced_dimension line 162
  21. theorem OAI.BinaryCoordinateSweeps.Young.hook_removal_dimension_upper line 172