OAI/Combinatorics/Progressions/Estimates/FreePrimitiveCriterion.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Erdos3.wordPolynomialLieRing line 17
  2. instance OAI.Erdos3.wordPolynomialLieAlgebra line 28
  3. theorem OAI.Erdos3.wordPolynomial_lie line 33
  4. def OAI.Erdos3.freeLieWordExpansion line 35
  5. theorem OAI.Erdos3.freeLieWordExpansion_of line 38
  6. theorem OAI.Erdos3.freeLieWordExpansion_tree line 42
  7. theorem OAI.Erdos3.freeLie_mk_single_tree line 52
  8. theorem OAI.Erdos3.freeLie_linear_induction line 67
  9. theorem OAI.Erdos3.dynkinProjection_freeLieWordExpansion line 88
  10. theorem OAI.Erdos3.freeLieWordExpansion_injective line 100
  11. def OAI.Erdos3.wordPolynomialEmbedding line 115
  12. theorem OAI.Erdos3.wordPolynomialEmbedding_injective line 119
  13. theorem OAI.Erdos3.wordPolynomialEmbedding_generator line 123
  14. def OAI.Erdos3.wordPolynomialEmbeddingLie line 138
  15. def OAI.Erdos3.freeLieAssociativeExpansion line 148
  16. theorem OAI.Erdos3.wordPolynomialEmbedding_comp_freeLie line 151
  17. theorem OAI.Erdos3.freeLieAssociativeExpansion_injective line 161
  18. theorem OAI.Erdos3.freeLie_eq_of_associative_eq line 166
  19. theorem OAI.Erdos3.freeLie_universalEnveloping_injective line 170
  20. def OAI.Erdos3.freeWord line 190
  21. theorem OAI.Erdos3.freeWord_of line 193
  22. theorem OAI.Erdos3.freeWord_coeff line 196
  23. theorem OAI.Erdos3.freeWord_single_symm line 205
  24. def OAI.Erdos3.freeWordLinearMap line 211
  25. theorem OAI.Erdos3.freeWordLinearMap_word line 217
  26. theorem OAI.Erdos3.freeAlgebra_linear_induction line 221
  27. theorem OAI.Erdos3.freeMonoid_induction_right line 231
  28. def OAI.Erdos3.freeDegree line 242
  29. theorem OAI.Erdos3.freeDegree_word line 245
  30. theorem OAI.Erdos3.freeDegree_one line 248
  31. theorem OAI.Erdos3.freeDegree_generator line 252
  32. theorem OAI.Erdos3.freeDegree_mul line 256
  33. theorem OAI.Erdos3.map_lieTreeEval line 289
  34. theorem OAI.Erdos3.lift_lieTreeEval line 295
  35. theorem OAI.Erdos3.dynkinProjection_lift line 300
  36. theorem OAI.Erdos3.rightBracketList_mem_lowerCentralSeries line 312
  37. theorem OAI.Erdos3.dynkinWord_mem_lowerCentralSeries line 328
  38. theorem OAI.Erdos3.dynkinWord_eq_zero_of_length_gt line 335
  39. theorem OAI.Erdos3.dynkinProjection_eq_zero_of_low_coeff_zero line 343
  40. theorem OAI.Erdos3.dynkinProjection_eq_of_low_coeff_eq line 356
  41. theorem OAI.Erdos3.lie_lift_eq_of_low_word_coeff_eq line 367
  42. def OAI.Erdos3.freeCoproduct line 385
  43. theorem OAI.Erdos3.freeCoproduct_generator line 389
  44. def OAI.Erdos3.freeAugmentation line 394
  45. theorem OAI.Erdos3.freeAugmentation_generator line 397
  46. def OAI.Erdos3.freeAntipodeOp line 400
  47. def OAI.Erdos3.freeAntipode line 403
  48. theorem OAI.Erdos3.freeAntipode_generator line 406
  49. theorem OAI.Erdos3.freeAntipode_one line 411
  50. theorem OAI.Erdos3.freeAntipode_mul line 415
  51. def OAI.Erdos3.FreePrimitive line 421
  52. theorem OAI.Erdos3.freePrimitive_generator line 424
  53. theorem OAI.Erdos3.FreePrimitive.add line 427
  54. theorem OAI.Erdos3.FreePrimitive.smul line 433
  55. theorem OAI.Erdos3.FreePrimitive.commutator line 438
  56. def OAI.Erdos3.freeScaleSeries line 454
  57. theorem OAI.Erdos3.freeScaleSeries_generator line 457
  58. theorem OAI.Erdos3.freeScaleSeries_word line 461
  59. def OAI.Erdos3.freeHomogeneousPart line 470
  60. theorem OAI.Erdos3.freeHomogeneousPart_apply line 473
  61. theorem OAI.Erdos3.freeHomogeneousPart_word line 476
  62. theorem OAI.Erdos3.freeDegree_homogeneousPart line 480
  63. theorem OAI.Erdos3.freeHomogeneousPart_comp line 494
  64. def OAI.Erdos3.freeTruncation line 512
  65. theorem OAI.Erdos3.freeTruncation_apply line 515
  66. theorem OAI.Erdos3.freeTruncation_word line 519
  67. theorem OAI.Erdos3.freeTruncation_idempotent line 525
  68. def OAI.Erdos3.wordTruncation line 548
  69. theorem OAI.Erdos3.wordTruncation_single line 551
  70. theorem OAI.Erdos3.wordTruncation_coeff line 557
  71. theorem OAI.Erdos3.wordTruncation_idempotent line 572
  72. theorem OAI.Erdos3.wordTruncation_mul line 578
  73. theorem OAI.Erdos3.wordTruncation_eq_iff line 596
  74. theorem OAI.Erdos3.dynkinProjection_wordTruncation line 613
  75. theorem OAI.Erdos3.lie_lift_eq_of_wordTruncation_eq line 620
  76. def OAI.Erdos3.freeAssociativeLieSubalgebra line 638
  77. theorem OAI.Erdos3.freeAssociativeLieSubalgebra_generator line 641
  78. def OAI.Erdos3.freeAntipodeConvolution line 645
  79. def OAI.Erdos3.freeDynkinConvolution line 648
  80. theorem OAI.Erdos3.freeAntipodeConvolution_one line 651
  81. theorem OAI.Erdos3.freeDynkinConvolution_one line 655
  82. theorem OAI.Erdos3.freeAntipodeConvolution_mul_generator line 659
  83. theorem OAI.Erdos3.freeDynkinConvolution_mul_generator line 669
  84. theorem OAI.Erdos3.freeAntipodeConvolution_eq_augmentation line 681
  85. theorem OAI.Erdos3.freeDynkinConvolution_mem line 697
  86. theorem OAI.Erdos3.FreePrimitive.dynkin_eq_degree line 726
  87. theorem OAI.Erdos3.FreePrimitive.mem_of_degree line 732
  88. theorem OAI.Erdos3.freeAugmentation_antipode line 751
  89. theorem OAI.Erdos3.FreePrimitive.augmentation_eq_zero line 765
  90. def OAI.Erdos3.freeDegreeInverse line 776
  91. theorem OAI.Erdos3.freeDegreeInverse_word line 779
  92. theorem OAI.Erdos3.freeAugmentation_word_of_ne_one line 783
  93. theorem OAI.Erdos3.freeDegreeInverse_degree line 789
  94. theorem OAI.Erdos3.freeDegree_lieTree line 808
  95. theorem OAI.Erdos3.freePrimitive_lieTree line 823
  96. theorem OAI.Erdos3.freeDegreeInverse_lieTree line 829
  97. theorem OAI.Erdos3.freeDegreeInverse_mem line 839
  98. theorem OAI.Erdos3.FreePrimitive.mem line 856
  99. theorem OAI.Erdos3.freePrimitive_of_mem line 863
  100. theorem OAI.Erdos3.freePrimitive_iff_mem line 878