OAI/RepresentationTheory/PartialPermutation/RankFillings.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PartialPermutation.Tableau.exists_rankEnumeration line 12
2. def OAI.PartialPermutation.Tableau.fiberPermutation line 28
3. lemma OAI.PartialPermutation.Tableau.fiberPermutation_apply line 33
4. lemma OAI.PartialPermutation.Tableau.fiberPermutation_rank line 37
5. lemma OAI.PartialPermutation.Tableau.fiberPermutation_injective line 41
6. lemma OAI.PartialPermutation.Tableau.rank_factorial_le_filling_count line 51
7. lemma OAI.PartialPermutation.Tableau.two_pow_pred_le_factorial line 69
8. lemma OAI.PartialPermutation.Tableau.power_count_sub_ranks_le_factorials line 81
9. lemma OAI.PartialPermutation.Tableau.rank_power_le_filling_count line 93