OAI/Probability/BinarySweep/YoungTheory/YoungPlacement.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Young.movePlacement line 13
  2. lemma OAI.BinaryCoordinateSweeps.Young.movePlacement_mul line 16
  3. lemma OAI.BinaryCoordinateSweeps.Young.movePlacement_one line 20
  4. def OAI.BinaryCoordinateSweeps.Young.placementRep line 22
  5. lemma OAI.BinaryCoordinateSweeps.Young.placementRep_basis line 30
  6. abbrev OAI.BinaryCoordinateSweeps.Young.Tail line 46
  7. lemma OAI.BinaryCoordinateSweeps.Young.perm_same_tail_tabloid line 48
  8. lemma OAI.BinaryCoordinateSweeps.Young.placement_extends line 67
  9. def OAI.BinaryCoordinateSweeps.Young.placementTabloid line 71
  10. lemma OAI.BinaryCoordinateSweeps.Young.placementTabloid_eq line 74
  11. lemma OAI.BinaryCoordinateSweeps.Young.placementTabloid_surjective line 80
  12. lemma OAI.BinaryCoordinateSweeps.Young.placementTabloid_move line 86
  13. def OAI.BinaryCoordinateSweeps.Young.spechtPlacement line 95
  14. lemma OAI.BinaryCoordinateSweeps.Young.spechtPlacement_injective line 100
  15. lemma OAI.BinaryCoordinateSweeps.Young.spechtPlacement_intertwines line 107
  16. theorem OAI.BinaryCoordinateSweeps.Young.specht_finrank_le_placements line 115
  17. lemma OAI.BinaryCoordinateSweeps.Young.card_tail line 119
  18. theorem OAI.BinaryCoordinateSweeps.Young.specht_finrank_le_power line 126
  19. lemma OAI.BinaryCoordinateSweeps.Young.col_lt_firstRow line 134
  20. lemma OAI.BinaryCoordinateSweeps.Young.placement_column_collision line 138
  21. def OAI.BinaryCoordinateSweeps.Young.columnSum line 157
  22. lemma OAI.BinaryCoordinateSweeps.Young.columnSum_apply line 160
  23. lemma OAI.BinaryCoordinateSweeps.Young.columnSum_rep line 164
  24. lemma OAI.BinaryCoordinateSweeps.Young.columnSum_placement_zero line 182
  25. theorem OAI.BinaryCoordinateSweeps.Young.no_short_placement_intertwiner line 211