OAI/Combinatorics/Progressions/Estimates/NativeRoundedCyclicModel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FreimanModel.exists_dense_cyclicProduct_model line 13
2. theorem OAI.Erdos3.FreimanModel.exists_cyclicProduct_model_with_fourfold_lift line 106
3. theorem OAI.Erdos3.FreimanModel.exists_roundedGraph_cyclic_model line 139
4. theorem OAI.Erdos3.FreimanModel.exists_variableRoundedGraph_cyclic_model line 216
5. theorem OAI.Erdos3.NativeRankRelation.CommonData.variable_graph_affine_model line 305
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.rounded_graph_cyclic_model line 390