OAI/RepresentationTheory/PartialPermutation/Tabloids.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartialPermutation.YoungTabloid.row line 12
  2. def OAI.PartialPermutation.YoungTabloid.col line 13
  3. def OAI.PartialPermutation.YoungTabloid.Tabloid line 15
  4. def OAI.PartialPermutation.YoungTabloid.ofPerm line 18
  5. lemma OAI.PartialPermutation.YoungTabloid.ofPerm_surjective line 21
  6. instance OAI.PartialPermutation.YoungTabloid.(instance at line 25) line 25
  7. instance OAI.PartialPermutation.YoungTabloid.(instance at line 27) line 27
  8. def OAI.PartialPermutation.YoungTabloid.canonical line 29
  9. def OAI.PartialPermutation.YoungTabloid.relabel line 31
  10. lemma OAI.PartialPermutation.YoungTabloid.relabel_apply line 36
  11. lemma OAI.PartialPermutation.YoungTabloid.relabel_one line 39
  12. lemma OAI.PartialPermutation.YoungTabloid.relabel_mul line 40
  13. def OAI.PartialPermutation.YoungTabloid.relabelEquiv line 46
  14. lemma OAI.PartialPermutation.YoungTabloid.rowSum line 52
  15. def OAI.PartialPermutation.YoungTabloid.columnGroup line 58
  16. def OAI.PartialPermutation.YoungTabloid.Col line 66
  17. instance OAI.PartialPermutation.YoungTabloid.(instance at line 68) line 68
  18. def OAI.PartialPermutation.YoungTabloid.columnEquiv line 70
  19. lemma OAI.PartialPermutation.YoungTabloid.col_card line 79