OAI/Combinatorics/Progressions/Estimates/CommonDependentWordLayers.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer line 13
  2. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer_antitone line 16
  3. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer_lie_mem line 20
  4. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer_zero line 26
  5. def OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayerIdeal line 47
  6. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer_le_degreeRank line 57
  7. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer_marked_terminal line 62
  8. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer_degree_terminal line 67
  9. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.of_mem_markedLayer line 73
  10. def OAI.Erdos3.FreeDegreeRankLieAlgebra.gradingHom line 90
  11. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.gradingHom_of line 99
  12. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.gradingHom_tree line 103
  13. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.gradingHom_eval_one line 114
  14. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.gradingHom_injective line 125
  15. def OAI.Erdos3.FreeDegreeRankLieAlgebra.gradingExpansion line 130
  16. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.homogeneousSpan_inter line 136
  17. theorem OAI.Erdos3.NilpotentLieFiltration.top_rank_map_mem_degreeLengthSpan line 151
  18. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.lift_layer_mem_degreeLengthSpan line 166
  19. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.lift_top_mem_degreeLengthSpan line 188
  20. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.lift_top_frequency_zero line 202
  21. def OAI.Erdos3.markedGradeRegion line 222
  22. theorem OAI.Erdos3.markedGradeRegion_inter line 225
  23. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer_eq_homogeneousSpan line 237
  24. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer_inf line 246
  25. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.markedLayer_separate_inter line 253
  26. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.topLayer_eq_markedLayer line 259
  27. theorem OAI.Erdos3.FreeDegreeRankLieAlgebra.topLayer_inter_markedIdeal line 279
  28. def OAI.Erdos3.NativeRankRelation.CommonData.coefficientLayerIndex line 306
  29. def OAI.Erdos3.NativeRankRelation.CommonData.coefficientIsDependent line 308
  30. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientWeight_eq_layerIndex line 310
  31. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientFreeGenerator_mem_combined line 314
  32. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientFreeGenerator_mem_dependent line 320
  33. def OAI.Erdos3.NativeRankRelation.CommonData.dependentWordLayer line 327
  34. def OAI.Erdos3.NativeRankRelation.CommonData.dependentWordIdeal line 331
  35. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentWordLayer_zero line 335
  36. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentWordLayer_antitone line 338
  37. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentWordLayer_lie_mem line 342
  38. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentWordLayer_le_degreeRank line 347
  39. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentWordLayer_marked_terminal line 352
  40. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonFreeSpan_le_dependentWordLayer line 357
  41. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentFreeSpan_le_dependentWordLayer line 364