OAI/Combinatorics/Progressions/Estimates/MultidegreeDilationPair.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.MultidegreeLieFiltration line 20
  2. def OAI.Erdos3.MultidegreeLieFiltration.layerIdeal line 33
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_layerIdeal line 41
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.layer_le_ordinary line 44
  5. abbrev OAI.Erdos3.MultidegreeLieFiltration.Group line 48
  6. def OAI.Erdos3.MultidegreeLieFiltration.subgroup line 50
  7. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_subgroup line 53
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.subgroup_normal line 56
  9. theorem OAI.Erdos3.MultidegreeLieFiltration.subgroup_antitone line 59
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.subgroup_le_ordinary line 61
  11. theorem OAI.Erdos3.MultidegreeLieFiltration.subgroup_commutator_mem line 64
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.subgroup_eq_bot line 69
  13. def OAI.Erdos3.multidegreeTotalLayer line 92
  14. theorem OAI.Erdos3.layer_le_multidegreeTotalLayer line 95
  15. theorem OAI.Erdos3.multidegreeTotalLayer_antitone line 99
  16. theorem OAI.Erdos3.multidegreeTotalLayer_eq line 106
  17. theorem OAI.Erdos3.multidegreeTotalLayer_lie_mem line 118
  18. theorem OAI.Erdos3.multidegreeTotalLayer_terminal line 139
  19. def OAI.Erdos3.MultidegreeLieFiltration.ofLayers line 152
  20. theorem OAI.Erdos3.multidegree_sum_lt_of_lt line 181
  21. def OAI.Erdos3.MultidegreeLieFiltration.strictUpperLayer line 192
  22. theorem OAI.Erdos3.MultidegreeLieFiltration.successor_le_strictUpperLayer line 195
  23. theorem OAI.Erdos3.MultidegreeLieFiltration.strictUpperLayer_le_layer line 199
  24. theorem OAI.Erdos3.MultidegreeLieFiltration.strictUpperLayer_antitone line 205
  25. theorem OAI.Erdos3.MultidegreeLieFiltration.layer_le_strictUpperLayer line 212
  26. theorem OAI.Erdos3.MultidegreeLieFiltration.strictUpperLayer_le_ordinary line 223
  27. theorem OAI.Erdos3.MultidegreeLieFiltration.strictUpperLayer_top line 236
  28. theorem OAI.Erdos3.MultidegreeLieFiltration.strictUpper_lie_layer line 250
  29. theorem OAI.Erdos3.MultidegreeLieFiltration.layer_lie_strictUpper line 265
  30. def OAI.Erdos3.multidegreeWeight line 284
  31. theorem OAI.Erdos3.multidegreeWeight_add line 286
  32. theorem OAI.Erdos3.multidegreeWeight_mono line 290
  33. def OAI.Erdos3.MultidegreeLieFiltration.weightedLayer line 299
  34. theorem OAI.Erdos3.MultidegreeLieFiltration.layer_le_weightedLayer line 302
  35. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedLayer_antitone line 306
  36. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedLayer_zero line 312
  37. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedLayer_terminal line 319
  38. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedLayer_lie_mem line 334
  39. theorem OAI.Erdos3.MultidegreeLieFiltration.pi_degree_eq line 372
  40. def OAI.Erdos3.MultidegreeLieFiltration.pi line 388
  41. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_pi_layer line 399
  42. def OAI.Erdos3.MultidegreeLieFiltration.piLayerEquiv line 404
  43. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeAdaptedModule line 424
  44. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_squarefreeAdaptedModule line 443
  45. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeMonomial_mem_adapted line 448
  46. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeMonomial_component_mem line 459
  47. def OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer line 480
  48. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_dilationPairLayer line 483
  49. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer_antitone line 487
  50. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer_lie_mem line 503
  51. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer_le_ordinary line 520
  52. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer_le_subalgebra line 526
  53. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer_terminal line 530
  54. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer_top_relation line 539
  55. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer_diagonal line 545
  56. theorem OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayer_of_strictUpper line 549
  57. def OAI.Erdos3.MultidegreeLieFiltration.dilationPairLayerEquiv line 555