OAI/RepresentationTheory/FoulkesSixth/HomogeneousPlethysm.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Foulkes.Complete.homogeneous_h line 11
2. lemma OAI.Foulkes.Complete.homogeneous_pleth line 17
3. lemma OAI.Foulkes.Lookup.degree_expVector line 31
4. lemma OAI.Foulkes.Lookup.homogeneous_alternant line 35
5. abbrev OAI.Foulkes.Lookup.Partition line 50
6. instance OAI.Foulkes.Lookup.(instance at line 53) line 53
7. def OAI.Foulkes.Lookup.partVec line 57
8. lemma OAI.Foulkes.Lookup.partVec_antitone line 59
9. lemma OAI.Foulkes.Lookup.partVec_sum line 61
10. def OAI.Foulkes.Lookup.unshift line 66
11. lemma OAI.Foulkes.Lookup.unshift_antitone line 68
12. lemma OAI.Foulkes.Lookup.shifted_unshift line 79
13. lemma OAI.Foulkes.Lookup.unshift_sum line 84
14. def OAI.Foulkes.Lookup.unshiftPartition line 91
15. lemma OAI.Foulkes.Lookup.partVec_injective line 96
16. lemma OAI.Foulkes.Lookup.shifted_injective line 103
17. theorem OAI.Foulkes.Lookup.homogeneous_schur_expansion line 108