OAI/Combinatorics/Progressions/Estimates/CommonMarkedMultidegree.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.mixedCorrelationDegree_sum line 12
  2. def OAI.Erdos3.markedShiftMultidegree line 21
  3. theorem OAI.Erdos3.markedShiftMultidegree_layer line 30
  4. theorem OAI.Erdos3.markedShiftMultidegree_lowerCentralSeries_eq_bot line 34
  5. abbrev OAI.Erdos3.MarkedMixedGroup line 39
  6. theorem OAI.Erdos3.markedMixedGroup_nilpotencyClass_le line 41
  7. theorem OAI.Erdos3.markedShiftMultidegree_top_central line 45
  8. theorem OAI.Erdos3.markedShiftMultidegree_top_rank_mem line 59
  9. def OAI.Erdos3.realMarkedDirection line 85
  10. theorem OAI.Erdos3.realMarkedDirection_double_lie line 88
  11. theorem OAI.Erdos3.realMarkedTranslate_first_order line 98
  12. theorem OAI.Erdos3.realMarkedTranslate_conjugation line 111
  13. theorem OAI.Erdos3.realMarkedTranslate_quotient line 122
  14. theorem OAI.Erdos3.realMarkedShiftEval_translate line 134
  15. theorem OAI.Erdos3.realMarkedTranslate_conjugation_lift line 144
  16. theorem OAI.Erdos3.markedQuotientDirection_smul line 168
  17. theorem OAI.Erdos3.realMarkedDirection_smul line 173
  18. theorem OAI.Erdos3.markedDirection_mem_realLattice_of_smul line 179
  19. def OAI.Erdos3.rationalMarkedDirectionMap line 202
  20. theorem OAI.Erdos3.rationalMarkedDirectionMap_apply line 206
  21. def OAI.Erdos3.realMarkedParameterDirection line 209
  22. theorem OAI.Erdos3.realMarkedParameterDirection_apply line 213
  23. theorem OAI.Erdos3.realMarkedParameterDirection_rat line 224
  24. theorem OAI.Erdos3.markedQuotientDirection_mem_first line 229
  25. theorem OAI.Erdos3.realMarkedDirection_mem_first line 238
  26. theorem OAI.Erdos3.realMarkedParameterDirection_mem_first line 243
  27. theorem OAI.Erdos3.marked_first_layer_bracket_zero line 268
  28. theorem OAI.Erdos3.realMarkedParameterDirection_lie line 286
  29. theorem OAI.Erdos3.realMarkedParameterDirection_double_lie line 293
  30. def OAI.Erdos3.realMarkedParameterElement line 304
  31. theorem OAI.Erdos3.realMarkedParameterElement_mul line 308
  32. theorem OAI.Erdos3.realMarkedParameterElement_inv line 320
  33. theorem OAI.Erdos3.realMarkedParameterElement_conjugation line 326
  34. def OAI.Erdos3.NativeRankRelation.CommonData.markedQuotientMultidegree line 352
  35. abbrev OAI.Erdos3.NativeRankRelation.CommonData.MarkedQuotientGroup line 360
  36. theorem OAI.Erdos3.NativeRankRelation.CommonData.markedQuotientGroup_nilpotencyClass_le line 362
  37. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_marked_multidegree_top_frequency line 368