OAI/RepresentationTheory/FoulkesSixth/Differential.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Foulkes.Differential.Poly line 10
  2. def OAI.Foulkes.Differential.shift line 12
  3. theorem OAI.Foulkes.Differential.shift_X line 15
  4. theorem OAI.Foulkes.Differential.derivation_sum_apply line 19
  5. theorem OAI.Foulkes.Differential.shift_eq_sum line 27
  6. theorem OAI.Foulkes.Differential.shift_commutator line 38
  7. def OAI.Foulkes.Differential.rowWeight line 46
  8. theorem OAI.Foulkes.Differential.euler line 49
  9. theorem OAI.Foulkes.Differential.shift_lowers line 62
  10. theorem OAI.Foulkes.Differential.pderiv_zero_degree line 77
  11. theorem OAI.Foulkes.Differential.shift_zero_degree line 86
  12. theorem OAI.Foulkes.Differential.shift_nilpotent line 91
  13. theorem OAI.Foulkes.Differential.shift_triple line 100
  14. theorem OAI.Foulkes.Differential.shift_kernel_zero line 121
  15. theorem OAI.Foulkes.Differential.shift_injOn line 154
  16. theorem OAI.Foulkes.Differential.nilpotence_raise line 164
  17. theorem OAI.Foulkes.Differential.shift_power_kernel_zero line 184
  18. theorem OAI.Foulkes.Differential.shift_raises line 243
  19. theorem OAI.Foulkes.Differential.shift_spectator line 258
  20. theorem OAI.Foulkes.Differential.shift_pow_raises line 273
  21. theorem OAI.Foulkes.Differential.shift_pow_spectator line 283
  22. def OAI.Foulkes.Differential.shiftSequence line 293
  23. theorem OAI.Foulkes.Differential.shiftSequence_kernel_zero line 299