OAI/Probability/BinarySweep/YoungTheory/YoungTranspose.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Young.signTwist line 14
2. def OAI.BinaryCoordinateSweeps.Young.signTwistSubrep line 22
3. instance OAI.BinaryCoordinateSweeps.Young.signTwist_irreducible line 33
4. def OAI.BinaryCoordinateSweeps.Young.transposeCells line 38
5. lemma OAI.BinaryCoordinateSweeps.Young.transpose_sign line 44
6. lemma OAI.BinaryCoordinateSweeps.Young.transpose_row_to_col line 47
7. lemma OAI.BinaryCoordinateSweeps.Young.transpose_col_to_row line 52
8. def OAI.BinaryCoordinateSweeps.Young.transposeRep line 57
9. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 60) line 60
10. lemma OAI.BinaryCoordinateSweeps.Young.transposePoly_row_fixed line 64
11. def OAI.BinaryCoordinateSweeps.Young.transposeMap line 71
12. lemma OAI.BinaryCoordinateSweeps.Young.transposeMap_intertwines line 74
13. lemma OAI.BinaryCoordinateSweeps.Young.row_fixes_base_evaluation line 80
14. lemma OAI.BinaryCoordinateSweeps.Young.transposeMap_poly_evaluation line 87
15. theorem OAI.BinaryCoordinateSweeps.Young.specht_transpose_sign line 110
16. lemma OAI.BinaryCoordinateSweeps.Young.specht_finrank_transpose line 128