OAI/Combinatorics/Progressions/Lattices/AllocatedProductGeometricAffine.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedUniformAccurateAffineData line 27
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedUniformCommonCover_accurate_affine line 52
  3. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_accurate_affine line 69
  4. def OAI.Erdos3.VectorPolynomial.AllocatedUniformNormalizedAffineData line 115
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedUniformAccurateAffine_normalized line 140
  6. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_normalized_affine line 161
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonNormalizedAffineAt_mono_width line 206
  8. def OAI.Erdos3.VectorPolynomial.AllocatedGeometricNormalizedAffineData line 217
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedUniformNormalizedAffine_geometric line 234
  10. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_geometric_normalized_affine line 257
  11. def OAI.Erdos3.VectorPolynomial.AllocatedUniformPrimitiveAffineData line 310
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedUniformNormalizedAffine_primitive line 335
  13. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_primitive_affine line 356
  14. def OAI.Erdos3.VectorPolynomial.AllocatedProductGeometricNormalizedAffineData line 402
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedUniformNormalizedAffine_product_geometric line 421
  16. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_product_geometric_normalized_affine line 444