OAI/Combinatorics/Progressions/Lattices/IntegerAffineResidues.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerJetMatrix line 15
  2. theorem OAI.Erdos3.integerJetMatrix_apply_coefficients line 20
  3. theorem OAI.Erdos3.integerJetMatrix_residue_eq line 33
  4. theorem OAI.Erdos3.integerJetMatrix_image_eq line 45
  5. def OAI.Erdos3.integerBooleanInterpolant line 67
  6. theorem OAI.Erdos3.integerBooleanInterpolant_eval line 71
  7. theorem OAI.Erdos3.integerBooleanInterpolant_jet line 94
  8. theorem OAI.Erdos3.integerBooleanInterpolant_degree line 105
  9. def OAI.Erdos3.integerAffineCube line 128
  10. def OAI.Erdos3.integerAffineNumerator line 131
  11. theorem OAI.Erdos3.integerAffineNumerator_eval line 135
  12. theorem OAI.Erdos3.integerAffineNumerator_boolean line 144
  13. theorem OAI.Erdos3.integerAffineNumerator_degree line 153
  14. theorem OAI.Erdos3.integerAffine_interpolation line 162
  15. theorem OAI.Erdos3.exists_integer_kernel_dual line 185
  16. theorem OAI.Erdos3.integerKernel_interpolation line 200
  17. def OAI.Erdos3.realAffineCube line 219
  18. def OAI.Erdos3.realAffineDualPolynomial line 222
  19. theorem OAI.Erdos3.realAffineDualPolynomial_eval line 227
  20. theorem OAI.Erdos3.realAffineDualPolynomial_boolean line 238
  21. theorem OAI.Erdos3.realAffineDualPolynomial_degree line 249
  22. theorem OAI.Erdos3.realPolynomialMass_neg line 259
  23. theorem OAI.Erdos3.realPolynomialMass_sub_le line 264
  24. theorem OAI.Erdos3.realAffineDualPolynomial_mass line 268
  25. def OAI.Erdos3.boundedDegreeIntegerJetMatrix line 301
  26. theorem OAI.Erdos3.boundedDegreeIntegerJetMatrix_period line 306
  27. theorem OAI.Erdos3.boundedDegreeIntegerJetMatrix_index_le line 339
  28. theorem OAI.Erdos3.integerScalarLattice_pow_le line 351
  29. theorem OAI.Erdos3.boundedDegreeIntegerJetMatrix_common_period line 359
  30. theorem OAI.Erdos3.boundedDegreeIntegerJetMatrix_residue_iff line 369
  31. theorem OAI.Erdos3.integerAffineCube_residue_eq line 393
  32. theorem OAI.Erdos3.boundedDegreeIntegerJetMatrix_residue_eq line 410
  33. theorem OAI.Erdos3.boundedDegreeIntegerJetMatrix_image_eq line 421