OAI/RepresentationTheory/PartialPermutation/ColumnSorting.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PartialPermutation.YoungTabloid.exists_sortingEquiv line 13
  2. lemma OAI.PartialPermutation.YoungTabloid.strictMono_fin_nat_le line 20
  3. def OAI.PartialPermutation.YoungTabloid.Transversal line 33
  4. lemma OAI.PartialPermutation.YoungTabloid.transversal_col_injective line 36
  5. def OAI.PartialPermutation.YoungTabloid.sortedColumn line 42
  6. lemma OAI.PartialPermutation.YoungTabloid.sortedColumn_mono line 47
  7. def OAI.PartialPermutation.YoungTabloid.fiberPermutation line 52
  8. lemma OAI.PartialPermutation.YoungTabloid.fiberPermutation_apply line 57
  9. lemma OAI.PartialPermutation.YoungTabloid.fiberPermutation_rank line 61
  10. def OAI.PartialPermutation.YoungTabloid.columnSorting line 65
  11. lemma OAI.PartialPermutation.YoungTabloid.columnSorting_mem line 69
  12. lemma OAI.PartialPermutation.YoungTabloid.columnSorting_row line 73
  13. lemma OAI.PartialPermutation.YoungTabloid.transversal_eq_column line 81
  14. lemma OAI.PartialPermutation.YoungTabloid.column_row_injective line 91
  15. lemma OAI.PartialPermutation.YoungTabloid.unique_column_of_transversal line 100