OAI/Probability/BinarySweep/YoungTheory/YoungTabloid.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinaryCoordinateSweeps.Young.G line 11
2. def OAI.BinaryCoordinateSweeps.Young.labels line 13
3. def OAI.BinaryCoordinateSweeps.Young.Tabloid line 15
4. def OAI.BinaryCoordinateSweeps.Young.tabloidOfPerm line 17
5. lemma OAI.BinaryCoordinateSweeps.Young.tabloidOfPerm_surjective line 19
6. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 23) line 23
7. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 24) line 24
8. def OAI.BinaryCoordinateSweeps.Young.actTabloid line 26
9. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 33) line 33
10. lemma OAI.BinaryCoordinateSweeps.Young.smul_tabloid_apply line 46
11. lemma OAI.BinaryCoordinateSweeps.Young.smul_tabloidOfPerm line 49
12. lemma OAI.BinaryCoordinateSweeps.Young.tabloidOfPerm_eq_iff line 55
13. lemma OAI.BinaryCoordinateSweeps.Young.tabloidOfPerm_row_mul line 67
14. def OAI.BinaryCoordinateSweeps.Young.tabloidRepresentation line 72
15. lemma OAI.BinaryCoordinateSweeps.Young.tabloidRepresentation_apply line 80
16. def OAI.BinaryCoordinateSweeps.Young.tabloidBasis line 83
17. lemma OAI.BinaryCoordinateSweeps.Young.rep_basis line 85