OAI/RepresentationTheory/FoulkesSixth/VanishingSteps.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Foulkes.Vanishing.binary_split line 11
  2. abbrev OAI.Foulkes.Vanishing.S line 53
  3. def OAI.Foulkes.Vanishing.rowLift line 55
  4. def OAI.Foulkes.Vanishing.tensorRows line 58
  5. def OAI.Foulkes.Vanishing.lin line 60
  6. lemma OAI.Foulkes.Vanishing.rowLift_lin line 62
  7. lemma OAI.Foulkes.Vanishing.renameRow_rowLift line 65
  8. lemma OAI.Foulkes.Vanishing.renameRow_tensorRows line 69
  9. def OAI.Foulkes.Vanishing.Symmetric line 76
  10. lemma OAI.Foulkes.Vanishing.symmetric_tensorRows line 79
  11. def OAI.Foulkes.Vanishing.oneSlot line 84
  12. lemma OAI.Foulkes.Vanishing.oneSlot_eq line 87
  13. lemma OAI.Foulkes.Vanishing.eval_pderiv_prod line 98
  14. lemma OAI.Foulkes.Vanishing.binary_coefficient line 120
  15. def OAI.Foulkes.Vanishing.freeBase line 168
  16. def OAI.Foulkes.Vanishing.freeFamily line 171
  17. lemma OAI.Foulkes.Vanishing.shift_freeBase line 175
  18. lemma OAI.Foulkes.Vanishing.freeBase_degree_last line 183
  19. lemma OAI.Foulkes.Vanishing.freeBase_degree_cast line 192
  20. lemma OAI.Foulkes.Vanishing.freeFamily_degree_last line 204
  21. lemma OAI.Foulkes.Vanishing.freeFamily_degree_cast line 215
  22. lemma OAI.Foulkes.Vanishing.shift_freeFamily line 228
  23. theorem OAI.Foulkes.Vanishing.freeFamily_zero line 253
  24. lemma OAI.Foulkes.Vanishing.lin_binary_split line 290
  25. def OAI.Foulkes.Vanishing.vecProduct line 297
  26. def OAI.Foulkes.Vanishing.ProductsVanish line 299
  27. lemma OAI.Foulkes.Vanishing.tensorRows_diag_product line 302
  28. lemma OAI.Foulkes.Vanishing.productsVanish_mul line 307
  29. lemma OAI.Foulkes.Vanishing.binary_step line 319
  30. lemma OAI.Foulkes.Vanishing.oneSlot_last line 333
  31. def OAI.Foulkes.Vanishing.commonPower line 338
  32. def OAI.Foulkes.Vanishing.fixedFunctional line 341
  33. lemma OAI.Foulkes.Vanishing.fixedFunctional_apply line 344
  34. lemma OAI.Foulkes.Vanishing.eval_freeFamily line 348
  35. lemma OAI.Foulkes.Vanishing.free_last_slot line 358