OAI/RepresentationTheory/PartialPermutation/CrossTableaux.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartialPermutation.YoungTabloid.rowMoment line 12
2. def OAI.PartialPermutation.YoungTabloid.CrossTransversal line 14
3. def OAI.PartialPermutation.YoungTabloid.crossSortedColumn line 17
4. lemma OAI.PartialPermutation.YoungTabloid.crossSortedColumn_mono line 23
5. def OAI.PartialPermutation.YoungTabloid.crossSorting line 30
6. lemma OAI.PartialPermutation.YoungTabloid.crossSorting_row line 34
7. lemma OAI.PartialPermutation.YoungTabloid.cross_rowMoment_le line 42
8. def OAI.PartialPermutation.YoungTabloid.rowFiberEquiv line 51
9. lemma OAI.PartialPermutation.YoungTabloid.shape_eq_of_row_equiv line 60
10. lemma OAI.PartialPermutation.YoungTabloid.cross_equal_moment_shape_eq line 71