OAI/Combinatorics/Progressions/Estimates/SquarefreePermutationFiltration.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.squarefreePermute_monomial_lie line 18
  2. theorem OAI.Erdos3.squarefreePermute_lie line 32
  3. def OAI.Erdos3.squarefreePermuteLie line 48
  4. theorem OAI.Erdos3.NilpotentLieFiltration.layer_eq_bot_above_step line 62
  5. def OAI.Erdos3.NilpotentLieFiltration.raiseStep line 68
  6. theorem OAI.Erdos3.NilpotentLieFiltration.raiseStep_layer line 75
  7. theorem OAI.Erdos3.NilpotentLieFiltration.raiseStep_realification_layer line 78
  8. def OAI.Erdos3.NilpotentLieFiltration.raiseStepOrbit line 81
  9. theorem OAI.Erdos3.NilpotentLieFiltration.raiseStepOrbit_log line 85
  10. theorem OAI.Erdos3.bchSubgroupCoordinates_changeStep line 95
  11. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeComponent line 126
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeComponent_apply line 141
  13. theorem OAI.Erdos3.MultidegreeLieFiltration.sum_squarefreeComponent line 145
  14. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeAlgebra_lowerCentralSeries_eq_bot line 153
  15. def OAI.Erdos3.NilpotentLieFiltration.dropTop line 170
  16. theorem OAI.Erdos3.NilpotentLieFiltration.dropTop_layer line 177
  17. theorem OAI.Erdos3.NilpotentLieFiltration.dropTop_realification_layer line 179
  18. theorem OAI.Erdos3.DegreeRankLieFiltration.rank_zero_top_eq_bot line 188
  19. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeMultidegreeLayer line 207
  20. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeDegreeLayer line 211
  21. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_squarefreeMultidegreeLayer line 215
  22. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_squarefreeDegreeLayer line 220
  23. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeMultidegreeLayer_antitone line 225
  24. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeDegreeLayer_antitone line 229
  25. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeMultidegreeLayer_lie_mem line 233
  26. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeDegreeLayer_lie_mem line 240
  27. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeMultidegreeLayer_le_degree line 248
  28. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeComponent_mem_multidegree line 255
  29. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeComponent_eq_zero_of_degree line 259
  30. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeDegreeLayer_one line 280
  31. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeDegreeLayer_terminal line 286
  32. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeOrdinaryFiltration line 297
  33. def OAI.Erdos3.MultidegreeLieFiltration.comparisonProductLayer line 316
  34. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonProductLayer_antitone line 319
  35. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonProductLayer_lie_mem line 322
  36. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonProductLayer_one line 327
  37. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonProductLayer_terminal line 333
  38. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeMultidegreeLayer_zero line 354
  39. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeMultidegreeLayer_terminal line 359
  40. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefree_degree_eq line 369
  41. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeMultidegreeFiltration line 391
  42. theorem OAI.Erdos3.MultidegreeLieFiltration.blockPermutation_symm line 413
  43. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreePermute_mem_adapted line 418
  44. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeBlockPermute line 431
  45. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBlockPermute_apply line 442
  46. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeLayerMap line 457
  47. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeLayerMap_zero line 465
  48. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeLayerMap_coe line 469
  49. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeLayerMap_mem line 474
  50. theorem OAI.Erdos3.MultidegreeLieFiltration.factorialBlockMonomial_mem_adapted line 496
  51. def OAI.Erdos3.MultidegreeLieFiltration.blockLayerMap line 515
  52. theorem OAI.Erdos3.MultidegreeLieFiltration.blockLayerMap_coe line 522
  53. theorem OAI.Erdos3.MultidegreeLieFiltration.blockLayerMap_mem_degree line 525
  54. theorem OAI.Erdos3.MultidegreeLieFiltration.blockLayerMap_permute line 539
  55. theorem OAI.Erdos3.SquarefreeIndex.permute_one line 562
  56. theorem OAI.Erdos3.SquarefreeIndex.permute_mul line 568
  57. theorem OAI.Erdos3.squarefreePermute_one line 574
  58. theorem OAI.Erdos3.squarefreePermute_mul line 582
  59. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBlockPermute_one line 597
  60. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBlockPermute_mul line 601
  61. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBlockPermute_mem_degree line 622
  62. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBlockPermute_mem_multidegree line 630
  63. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBlockPermute_mem_topDegree line 637