OAI/Combinatorics/Progressions/Estimates/SquarefreeRealAction.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.comparisonGraph line 20
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraph_apply line 24
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraph_mem_degree line 27
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraph_lie line 33
  5. def OAI.Erdos3.MultidegreeLieFiltration.comparisonGraphLayer line 52
  6. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraph_mem_graphLayer line 57
  7. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraphLayer_induction line 67
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraphLayer_antitone line 82
  9. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraphLayer_le_degree line 91
  10. def OAI.Erdos3.MultidegreeLieFiltration.comparisonLayer line 114
  11. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonLayer_antitone line 117
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonLayer_le_product line 122
  13. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonLayer_zero line 126
  14. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonLayer_terminal line 129
  15. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonGraph_mem_layer line 133
  16. theorem OAI.Erdos3.map_mem_submodule_of_basis line 150
  17. theorem OAI.Erdos3.MultidegreeLieFiltration.comparisonLayer_le_of_generators line 165
  18. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeFinBasis line 202
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeFinBasis_structure_height line 206
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeFinBasis_multidegree_height line 212
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeFinBasis_degree_height line 219
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.blockLayerMap_chosen_height line 240
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonGraph_chosen_height line 294
  24. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeModel line 325
  25. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeModelMultidegree line 343
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeModel_complexity line 351
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_comparison_layer_basis_height line 382
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_squarefree_model line 466
  29. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeRealPermute line 503
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeRealPermute_one line 511
  31. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeRealPermute_mul line 516
  32. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeRealPermute_lattice line 523
  33. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeRealPermute_top line 532