OAI/RepresentationTheory/FoulkesSixth/Vanishing.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Foulkes.Vanishing.extendPerm line 11
2. lemma OAI.Foulkes.Vanishing.extendPerm_castSucc line 17
3. lemma OAI.Foulkes.Vanishing.extendPerm_last line 20
4. def OAI.Foulkes.Vanishing.embedRows line 23
5. lemma OAI.Foulkes.Vanishing.embedRows_rowLift line 26
6. lemma OAI.Foulkes.Vanishing.embedRows_rowForm line 30
7. lemma OAI.Foulkes.Vanishing.embedRows_pureRows line 33
8. lemma OAI.Foulkes.Vanishing.embedRows_tensorRows line 37
9. lemma OAI.Foulkes.Vanishing.renameRow_embedRows line 41
10. lemma OAI.Foulkes.Vanishing.renameRow_commonPower line 45
11. def OAI.Foulkes.Vanishing.restrictionFunctional line 50
12. lemma OAI.Foulkes.Vanishing.restrictionFunctional_apply line 54
13. lemma OAI.Foulkes.Vanishing.restriction_symmetric line 59
14. lemma OAI.Foulkes.Vanishing.restriction_products line 66
15. lemma OAI.Foulkes.Vanishing.eval_cast_rowLinear line 75
16. lemma OAI.Foulkes.Vanishing.eval_induction_family_univ line 82
17. lemma OAI.Foulkes.Vanishing.eval_induction_family_empty line 92
18. lemma OAI.Foulkes.Vanishing.remove_common_power line 99
19. theorem OAI.Foulkes.Vanishing.vanishing line 129
20. lemma OAI.Foulkes.Vanishing.average_renameRow line 172
21. theorem OAI.Foulkes.Vanishing.quadratic_bound line 178
22. theorem OAI.Foulkes.Vanishing.sixth_quadratic_bound line 207