OAI/RepresentationTheory/FoulkesSixth/IndependentChart.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Foulkes.Chart.dehom line 12
  2. lemma OAI.Foulkes.Chart.dehom_X_zero line 15
  3. lemma OAI.Foulkes.Chart.dehom_X_succ line 17
  4. lemma OAI.Foulkes.Chart.dehom_rowForm line 20
  5. lemma OAI.Foulkes.Chart.dehom_z_cons line 24
  6. lemma OAI.Foulkes.Chart.dehom_renameRow line 28
  7. def OAI.Foulkes.Chart.E line 36
  8. lemma OAI.Foulkes.Chart.dehom_z_mem_E line 38
  9. lemma OAI.Foulkes.Chart.one_mem_E line 41
  10. lemma OAI.Foulkes.Chart.pow_mono line 45
  11. lemma OAI.Foulkes.Chart.elementary_mem_E line 48
  12. lemma OAI.Foulkes.Chart.powersum_mem line 77
  13. def OAI.Foulkes.Chart.inRow line 112
  14. def OAI.Foulkes.Chart.pSum line 115
  15. lemma OAI.Foulkes.Chart.pSum_apply line 118
  16. lemma OAI.Foulkes.Chart.pSum_homogeneous_mem line 122
  17. lemma OAI.Foulkes.Chart.distinctSum_homogeneous_mem line 137
  18. def OAI.Foulkes.Chart.rowExp line 170
  19. lemma OAI.Foulkes.Chart.rowExp_apply line 173
  20. lemma OAI.Foulkes.Chart.monomial_eq_prod_rows line 176
  21. lemma OAI.Foulkes.Chart.renameRow_inRow line 182
  22. lemma OAI.Foulkes.Chart.permSum_monomial line 186
  23. lemma OAI.Foulkes.Chart.average_monomial_mem line 194
  24. def OAI.Foulkes.Chart.tailExp line 213
  25. lemma OAI.Foulkes.Chart.tailExp_apply line 216
  26. def OAI.Foulkes.Chart.rehomExp line 219
  27. lemma OAI.Foulkes.Chart.rehomExp_tailExp line 224
  28. lemma OAI.Foulkes.Chart.dehom_monomial line 235
  29. def OAI.Foulkes.Chart.rehom line 246
  30. lemma OAI.Foulkes.Chart.rehom_monomial line 249
  31. lemma OAI.Foulkes.Chart.rehom_dehom line 253
  32. lemma OAI.Foulkes.Chart.dehom_injective_W line 260
  33. lemma OAI.Foulkes.Chart.mul_mem_W line 269
  34. lemma OAI.Foulkes.Chart.one_mem_W line 273
  35. theorem OAI.Foulkes.Chart.invariant_mem_E_pow line 276
  36. lemma OAI.Foulkes.Chart.dehom_average line 288
  37. lemma OAI.Foulkes.Chart.dehom_R_mem_E_pow line 292
  38. def OAI.Foulkes.Chart.component line 315
  39. lemma OAI.Foulkes.Chart.E_pow_le_component_image line 317
  40. theorem OAI.Foulkes.Chart.chart_standard line 336
  41. def OAI.Foulkes.Chart.columns line 353
  42. def OAI.Foulkes.Chart.rowLinear line 356
  43. lemma OAI.Foulkes.Chart.rowLinear_apply line 361
  44. lemma OAI.Foulkes.Chart.columns_X line 364
  45. lemma OAI.Foulkes.Chart.rowForm_single line 368
  46. lemma OAI.Foulkes.Chart.columns_rowForm line 373
  47. lemma OAI.Foulkes.Chart.columns_pureRows line 385
  48. lemma OAI.Foulkes.Chart.columns_mem_W line 389
  49. lemma OAI.Foulkes.Chart.columns_renameRow line 400
  50. lemma OAI.Foulkes.Chart.columns_mem_R line 408
  51. lemma OAI.Foulkes.Chart.columns_mem_A line 413
  52. lemma OAI.Foulkes.Chart.columns_z line 421
  53. lemma OAI.Foulkes.Chart.columns_inverse line 424
  54. lemma OAI.Foulkes.Chart.exists_linearEquiv_send line 434
  55. theorem OAI.Foulkes.Chart.chart line 448
  56. lemma OAI.Foulkes.Chart.z_zero line 473
  57. theorem OAI.Foulkes.Chart.independent_chart_bound line 476