OAI/Combinatorics/Progressions/Polynomial/DegreeRankSunflower.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.DegreeRankLieFiltration line 13
  2. theorem OAI.Erdos3.DegreeRankLieFiltration.degree_antitone line 28
  3. theorem OAI.Erdos3.DegreeRankLieFiltration.rank_antitone line 34
  4. theorem OAI.Erdos3.DegreeRankLieFiltration.zero_eq_top line 38
  5. theorem OAI.Erdos3.DegreeRankLieFiltration.layer_eq_bot_of_past_top line 43
  6. def OAI.Erdos3.DegreeRankLieFiltration.associatedDegree line 53
  7. theorem OAI.Erdos3.DegreeRankLieFiltration.associatedDegree_layer line 60
  8. theorem OAI.Erdos3.DegreeRankLieFiltration.layer_le_associatedDegree line 62
  9. def OAI.Erdos3.NilpotentLieFiltration.canonicalDegreeRank line 71
  10. theorem OAI.Erdos3.NilpotentLieFiltration.canonicalDegreeRank_associatedDegree_layer line 81
  11. def OAI.Erdos3.DegreeRankLieFiltration.pi line 97
  12. theorem OAI.Erdos3.DegreeRankLieFiltration.mem_pi_layer line 109
  13. theorem OAI.Erdos3.DegreeRankLieFiltration.pi_associatedDegree line 114
  14. def OAI.Erdos3.DegreeRankLieFiltration.piLayerEquiv line 117
  15. def OAI.Erdos3.DegreeRankLieFiltration.rankFlag line 137
  16. theorem OAI.Erdos3.DegreeRankLieFiltration.rankFlag_antitone line 139
  17. theorem OAI.Erdos3.DegreeRankLieFiltration.rankFlag_zero line 150
  18. theorem OAI.Erdos3.DegreeRankLieFiltration.rankFlag_mul line 153
  19. theorem OAI.Erdos3.DegreeRankLieFiltration.rankFlag_terminal line 156
  20. theorem OAI.Erdos3.DegreeRankLieFiltration.rankFlag_lie_mem line 160
  21. theorem OAI.Erdos3.FilteredLieTree.map_eval_mem_degreeRank line 187
  22. theorem OAI.Erdos3.NilpotentLieFiltration.map_rankLayer line 198
  23. def OAI.Erdos3.NilpotentLieFiltration.rankSubgroup line 220
  24. theorem OAI.Erdos3.NilpotentLieFiltration.mem_rankSubgroup line 223
  25. theorem OAI.Erdos3.NilpotentLieFiltration.rankSubgroup_normal line 226
  26. theorem OAI.Erdos3.NilpotentLieFiltration.rankSubgroup_le_subgroup line 229
  27. theorem OAI.Erdos3.NilpotentLieFiltration.rankSubgroup_zero line 232
  28. theorem OAI.Erdos3.NilpotentLieFiltration.rankSubgroup_one line 237
  29. theorem OAI.Erdos3.NilpotentLieFiltration.rankSubgroup_lex_antitone line 242
  30. theorem OAI.Erdos3.NilpotentLieFiltration.rankSubgroup_overshoot line 245
  31. theorem OAI.Erdos3.NilpotentLieFiltration.rankSubgroup_commutator_mem line 251
  32. theorem OAI.Erdos3.NilpotentLieFiltration.rankSubgroup_eq_bot_of_degree_gt line 257
  33. theorem OAI.Erdos3.NilpotentLieFiltration.rankSubgroup_top_terminal line 267
  34. def OAI.Erdos3.DegreeRankLieFiltration.polynomialFiltration line 283
  35. theorem OAI.Erdos3.DegreeRankLieFiltration.polynomialFiltration_layer line 311
  36. theorem OAI.Erdos3.DegreeRankLieFiltration.monomial_mem_polynomialFiltration line 314
  37. theorem OAI.Erdos3.DegreeRankLieFiltration.lieTreeEval_mem line 330
  38. theorem OAI.Erdos3.DegreeRankLieFiltration.lieTreeEval_mem_length line 337
  39. theorem OAI.Erdos3.DegreeRankLieFiltration.lieTreeEval_sub_mem line 344
  40. theorem OAI.Erdos3.DegreeRankLieFiltration.top_lieTreeEval_congr line 365
  41. theorem OAI.Erdos3.DegreeRankLieFiltration.rankFlag_encode line 385
  42. theorem OAI.Erdos3.DegreeRankLieFiltration.rankFlag_encode_lt line 393
  43. theorem OAI.Erdos3.DegreeRankLieFiltration.rankFlag_decode_lt line 398
  44. theorem OAI.Erdos3.DegreeRankLieFiltration.layer_eq_rankFlag line 405
  45. def OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalKernel line 429
  46. abbrev OAI.Erdos3.DegreeRankLieFiltration.HigherHorizontal line 432
  47. def OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalMk line 434
  48. theorem OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalMk_eq line 437
  49. theorem OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalMk_surjective line 441
  50. def OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalRepresentative line 444
  51. theorem OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalRepresentative_zero line 448
  52. theorem OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalMk_representative line 453
  53. def OAI.Erdos3.DegreeRankLieFiltration.horizontalTreeValue line 461
  54. theorem OAI.Erdos3.DegreeRankLieFiltration.horizontalTreeValue_mem line 465
  55. theorem OAI.Erdos3.DegreeRankLieFiltration.horizontalTreeValue_mk line 470
  56. theorem OAI.Erdos3.DegreeRankLieFiltration.horizontalTreeValue_zero_of_leaf line 480
  57. def OAI.Erdos3.DegreeRankLieFiltration.fourHorizontalLayer line 497
  58. theorem OAI.Erdos3.DegreeRankLieFiltration.mem_fourHorizontalLayer line 500
  59. def OAI.Erdos3.DegreeRankLieFiltration.fourHorizontalMap line 504
  60. def OAI.Erdos3.DegreeRankLieFiltration.fourHorizontalImage line 516
  61. theorem OAI.Erdos3.DegreeRankLieFiltration.mem_fourHorizontalImage line 520
  62. theorem OAI.Erdos3.DegreeRankLieFiltration.fourHorizontalImage_frequency line 525
  63. theorem OAI.Erdos3.DegreeRankLieFiltration.sunflower_horizontal_bracket line 573
  64. theorem OAI.Erdos3.DegreeRankLieFiltration.sunflower_representative_bracket line 589