OAI/RepresentationTheory/FoulkesSixth/QuadraticInjection.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Foulkes.symAddCommGroup line 14
  2. instance OAI.Foulkes.symModule line 15
  3. instance OAI.Foulkes.symFinite line 16
  4. instance OAI.Foulkes.symFree line 18
  5. def OAI.Foulkes.Canonical.firstEquiv line 28
  6. def OAI.Foulkes.Canonical.firstMap line 31
  7. lemma OAI.Foulkes.Canonical.firstMap_mem line 34
  8. lemma OAI.Foulkes.Canonical.firstMap_power line 37
  9. def OAI.Foulkes.Canonical.productPolynomial line 46
  10. lemma OAI.Foulkes.Canonical.productPolynomial_power line 49
  11. lemma OAI.Foulkes.Canonical.productPolynomial_mem line 53
  12. lemma OAI.Foulkes.Canonical.productPolynomial_project line 68
  13. lemma OAI.Foulkes.Canonical.products_in_range line 74
  14. theorem OAI.Foulkes.Canonical.productPolynomial_range line 81
  15. def OAI.Foulkes.Canonical.map line 109
  16. lemma OAI.Foulkes.Canonical.map_polynomial line 113
  17. theorem OAI.Foulkes.Canonical.surjective line 119
  18. def OAI.Foulkes.Canonical.substitution line 140
  19. lemma OAI.Foulkes.Canonical.linearPolynomial_basis line 144
  20. lemma OAI.Foulkes.Canonical.substitution_row_linear line 149
  21. lemma OAI.Foulkes.Canonical.substitution_rowForm line 161
  22. lemma OAI.Foulkes.Canonical.substitution_z line 165
  23. lemma OAI.Foulkes.Canonical.row_polynomial_natural line 169
  24. lemma OAI.Foulkes.Canonical.tensorMap_natural line 181
  25. lemma OAI.Foulkes.Canonical.invariantMap_natural line 193
  26. lemma OAI.Foulkes.Canonical.firstMap_natural line 200
  27. lemma OAI.Foulkes.Canonical.productPolynomial_natural line 210
  28. theorem OAI.Foulkes.Canonical.natural line 221
  29. lemma OAI.Foulkes.PlethDual.natural_congr line 233
  30. def OAI.Foulkes.Injection.map line 256
  31. lemma OAI.Foulkes.Injection.adjoint line 261
  32. lemma OAI.Foulkes.Injection.injective line 271
  33. theorem OAI.Foulkes.Injection.natural line 278
  34. theorem OAI.Foulkes.Injection.quadratic_comparison line 298
  35. theorem OAI.Foulkes.Injection.sixth_large line 305