OAI/RepresentationTheory/FoulkesSixth/InvariantPolarization.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Foulkes.Polarization.renameRow line 11
  2. lemma OAI.Foulkes.Polarization.renameRow_comp line 14
  3. lemma OAI.Foulkes.Polarization.renameRow_rowForm line 18
  4. lemma OAI.Foulkes.Polarization.renameRow_pureRows line 22
  5. lemma OAI.Foulkes.Polarization.renameRow_mem_W line 29
  6. lemma OAI.Foulkes.Polarization.renameRow_z line 41
  7. def OAI.Foulkes.Polarization.rowInvariants line 46
  8. def OAI.Foulkes.Polarization.R line 54
  9. def OAI.Foulkes.Polarization.A line 56
  10. def OAI.Foulkes.Polarization.average line 58
  11. lemma OAI.Foulkes.Polarization.average_apply line 61
  12. lemma OAI.Foulkes.Polarization.average_invariant line 65
  13. lemma OAI.Foulkes.Polarization.average_mem_R line 71
  14. lemma OAI.Foulkes.Polarization.average_eq line 81
  15. lemma OAI.Foulkes.Polarization.average_zpow_mul line 89
  16. lemma OAI.Foulkes.Polarization.z_mem_R line 94
  17. lemma OAI.Foulkes.Polarization.z_mem_A line 99
  18. def OAI.Foulkes.Polarization.invariantPolarizedSpan line 102
  19. theorem OAI.Foulkes.Polarization.R_polarization line 106
  20. def OAI.Foulkes.Polarization.lowDegreeModule line 129
  21. theorem OAI.Foulkes.Polarization.module_generation line 132
  22. lemma OAI.Foulkes.Polarization.A_le_rowInvariants line 150
  23. lemma OAI.Foulkes.Polarization.AComponent_le_R line 155