OAI/Combinatorics/Progressions/Lattices/NativeProperAffineRecovery.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FreimanModel.residueBlock line 17
  2. def OAI.Erdos3.FreimanModel.residueLift line 22
  3. theorem OAI.Erdos3.FreimanModel.residueBlock_bounds line 24
  4. theorem OAI.Erdos3.FreimanModel.residueLift_sum_cast line 35
  5. theorem OAI.Erdos3.FreimanModel.residueLift_sum_bounds line 43
  6. theorem OAI.Erdos3.FreimanModel.residueLift_sum_sub_abs_lt line 64
  7. theorem OAI.Erdos3.FreimanModel.residueLift_sum_eq_iff line 76
  8. def OAI.Erdos3.FreimanModel.cyclicProductLift line 103
  9. def OAI.Erdos3.FreimanModel.cyclicProductBlock line 105
  10. theorem OAI.Erdos3.FreimanModel.cyclicProductLift_injective line 107
  11. theorem OAI.Erdos3.FreimanModel.cyclicProductLift_sum_apply line 114
  12. theorem OAI.Erdos3.FreimanModel.cyclicProduct_sum_apply line 121
  13. theorem OAI.Erdos3.FreimanModel.cyclicProductLift_sum_eq_iff line 127
  14. theorem OAI.Erdos3.FreimanModel.isAddFreimanIso_cyclicProductLift line 157
  15. theorem OAI.Erdos3.FreimanModel.exists_large_cyclicProduct_integer_lift line 171
  16. theorem OAI.Erdos3.FreimanModel.exists_dense_cyclic_model_of_integer_vectors line 196
  17. theorem OAI.Erdos3.FreimanModel.exists_dense_cyclicProduct_integer_model line 269
  18. def OAI.Erdos3.FreimanModel.variableIntegerGraphLift line 373
  19. def OAI.Erdos3.FreimanModel.variableIntegerGraphReduction line 378
  20. theorem OAI.Erdos3.FreimanModel.variableIntegerGraphReduction_lift line 384
  21. theorem OAI.Erdos3.FreimanModel.variableIntegerGraphLift_none line 394
  22. theorem OAI.Erdos3.FreimanModel.variableIntegerGraphLift_some line 398
  23. theorem OAI.Erdos3.FreimanModel.variableIntegerGraphLift_injective line 402
  24. theorem OAI.Erdos3.FreimanModel.exists_variableIntegerGraph_cyclic_model line 408
  25. theorem OAI.Erdos3.FreimanModel.exists_bounded_affine_box_of_cyclic_model line 459
  26. theorem OAI.Erdos3.NativeRankRelation.CommonData.integer_graph_affine_model line 532
  27. theorem OAI.Erdos3.NativeRankRelation.CommonData.integer_affine_graph_recovery line 642
  28. theorem OAI.Erdos3.NativeRankRelation.CommonData.proper_integer_graph_affine_model line 728
  29. theorem OAI.Erdos3.NativeRankRelation.CommonData.proper_affine_graph_recovery line 801