OAI/Probability/ThorpShuffle/Irreducibility.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thorp.Young.Standard line 17
2. lemma OAI.Thorp.Young.standard_row_lt_iff line 19
3. lemma OAI.Thorp.Young.standard_col_lt_iff line 35
4. lemma OAI.Thorp.Young.column_eq_rowRank line 51
5. lemma OAI.Thorp.Young.standard_eq_of_rows line 70
6. theorem OAI.Thorp.Specht.independent_of_leading line 84
7. lemma OAI.Thorp.Specht.column_word_le line 121
8. def OAI.Thorp.Specht.movedTableau line 155
9. def OAI.Thorp.Specht.StandardPerm line 157
10. instance OAI.Thorp.Specht.(instance at line 159) line 159
11. def OAI.Thorp.Specht.movedWord line 161
12. lemma OAI.Thorp.Specht.movedWord_apply line 163
13. lemma OAI.Thorp.Specht.moved_diag line 166
14. lemma OAI.Thorp.Specht.moved_leading line 172
15. lemma OAI.Thorp.Specht.standardWord_injective line 194
16. theorem OAI.Thorp.Specht.standard_polytabloids_independent line 206
17. def OAI.Thorp.Specht.orbitVector line 216
18. theorem OAI.Thorp.Specht.standardPerm_card_le_degree line 220