OAI/RepresentationTheory/PartialPermutation/TableauVectors.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PartialPermutation.YoungTabloid.Std line 14
  2. def OAI.PartialPermutation.YoungTabloid.referenceLabels line 16
  3. def OAI.PartialPermutation.YoungTabloid.tableauPerm line 17
  4. def OAI.PartialPermutation.YoungTabloid.tableauTabloid line 19
  5. def OAI.PartialPermutation.YoungTabloid.tableauVector line 21
  6. def OAI.PartialPermutation.YoungTabloid.rowCell line 24
  7. lemma OAI.PartialPermutation.YoungTabloid.rowCell_strictMono line 27
  8. lemma OAI.PartialPermutation.YoungTabloid.standard_eq_of_inverse_rows line 34
  9. lemma OAI.PartialPermutation.YoungTabloid.tableauTabloid_injective line 68
  10. def OAI.PartialPermutation.YoungTabloid.score line 75
  11. lemma OAI.PartialPermutation.YoungTabloid.score_relabel line 78
  12. lemma OAI.PartialPermutation.YoungTabloid.score_tableau_column line 84
  13. lemma OAI.PartialPermutation.YoungTabloid.score_tableau line 92
  14. lemma OAI.PartialPermutation.YoungTabloid.score_column_le line 97
  15. lemma OAI.PartialPermutation.YoungTabloid.score_column_eq line 103