OAI/RepresentationTheory/PartialPermutation/ColumnRearrangement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PartialPermutation.YoungTabloid.cell_eq_of_row_col line 12
2. lemma OAI.PartialPermutation.YoungTabloid.cell_lt_of_column line 16
3. def OAI.PartialPermutation.YoungTabloid.columnRestrict line 23
4. lemma OAI.PartialPermutation.YoungTabloid.column_monovary line 29
5. lemma OAI.PartialPermutation.YoungTabloid.column_rearrangement line 34
6. lemma OAI.PartialPermutation.YoungTabloid.fin_perm_mono_eq line 39
7. lemma OAI.PartialPermutation.YoungTabloid.column_rearrangement_eq line 48
8. def OAI.PartialPermutation.YoungTabloid.colIndex line 77
9. def OAI.PartialPermutation.YoungTabloid.columnDecomp line 81
10. lemma OAI.PartialPermutation.YoungTabloid.sum_columns line 91
11. lemma OAI.PartialPermutation.YoungTabloid.full_rearrangement line 97
12. lemma OAI.PartialPermutation.YoungTabloid.full_rearrangement_eq line 103