OAI/RepresentationTheory/FoulkesSixth/SymTensors.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Foulkes.symmetricTensors line 12
  2. abbrev OAI.Foulkes.Sym line 20
  3. def OAI.Foulkes.symMap line 23
  4. abbrev OAI.Foulkes.SymmetricTensor.T line 34
  5. def OAI.Foulkes.SymmetricTensor.perm line 36
  6. lemma OAI.Foulkes.SymmetricTensor.perm_mul line 39
  7. def OAI.Foulkes.SymmetricTensor.average line 43
  8. lemma OAI.Foulkes.SymmetricTensor.average_apply line 46
  9. lemma OAI.Foulkes.SymmetricTensor.average_invariant line 50
  10. lemma OAI.Foulkes.SymmetricTensor.average_perm line 57
  11. lemma OAI.Foulkes.SymmetricTensor.average_eq line 63
  12. def OAI.Foulkes.SymmetricTensor.project line 70
  13. lemma OAI.Foulkes.SymmetricTensor.project_coe line 73
  14. lemma OAI.Foulkes.SymmetricTensor.project_perm line 77
  15. def OAI.Foulkes.SymmetricTensor.power line 82
  16. lemma OAI.Foulkes.SymmetricTensor.coe_power line 85
  17. lemma OAI.Foulkes.SymmetricTensor.project_power line 88
  18. theorem OAI.Foulkes.SymmetricTensor.span_power line 92
  19. lemma OAI.Foulkes.symMap_power line 120
  20. lemma OAI.Foulkes.symMap_ext line 127
  21. lemma OAI.Foulkes.symMap_comp line 135
  22. lemma OAI.Foulkes.symMap_id line 143