OAI/RepresentationTheory/PartialPermutation/SpechtClassification.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartialPermutation.SpechtActual.labels line 18
2. def OAI.PartialPermutation.SpechtActual.rep line 21
3. instance OAI.PartialPermutation.SpechtActual.(instance at line 24) line 24
4. def OAI.PartialPermutation.SpechtActual.index line 28
5. lemma OAI.PartialPermutation.SpechtActual.index_spec line 31
6. lemma OAI.PartialPermutation.SpechtActual.rep_equiv_shape_eq line 35
7. lemma OAI.PartialPermutation.SpechtActual.index_injective line 49
8. lemma OAI.PartialPermutation.SpechtActual.actual_irreducible_card_le line 56
9. theorem OAI.PartialPermutation.SpechtActual.index_bijective line 62
10. def OAI.PartialPermutation.SpechtActual.indexEquiv line 68
11. lemma OAI.PartialPermutation.SpechtActual.standardCount_le_degree line 71