OAI/Combinatorics/Progressions/Polynomial/CRTPolynomialInputStepLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.crtPolynomialInputLaw_product_step_uniform line 18
  2. theorem OAI.Erdos3.crtPolynomialInputLaw_divisor_affine line 45
  3. theorem OAI.Erdos3.crtPolynomialInputLaw_divisor_complexMean line 58
  4. theorem OAI.Erdos3.tupleResidueReduction_integer_lift line 83
  5. theorem OAI.Erdos3.crtPolynomialInputLaw_divisor_integerOrigin_complexMean line 97
  6. theorem OAI.Erdos3.padicStepQuotient_coprime line 123
  7. def OAI.Erdos3.padicStepQuotientUnit line 135
  8. theorem OAI.Erdos3.padicStepQuotientUnit_coe line 140
  9. theorem OAI.Erdos3.padicStepQuotientUnit_factor line 145
  10. def OAI.Erdos3.prescribedCRTArbitraryStepEquiv line 154
  11. theorem OAI.Erdos3.prescribedCRTArbitraryStepEquiv_local_step line 170
  12. theorem OAI.Erdos3.prescribedCRTPolynomialInput_arbitrary_step line 181
  13. theorem OAI.Erdos3.crtPolynomialInputLaw_arbitrary_step_uniform line 205
  14. theorem OAI.Erdos3.crtInput_intCast_apply line 234
  15. theorem OAI.Erdos3.uniform_affine_valuationProduct_eq_step line 240
  16. theorem OAI.Erdos3.crtPolynomialInputLaw_arbitrary_step_divisor_affine line 256
  17. theorem OAI.Erdos3.crtPolynomialInputLaw_arbitrary_step_divisor_complexMean line 273