OAI/Combinatorics/Progressions/Lattices/CRTPrescribedProductStep.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.prescribedCRTCofactor line 14
  2. theorem OAI.Erdos3.prescribedCRTProductStep_eq line 17
  3. theorem OAI.Erdos3.prescribedCRTCofactor_coprime line 22
  4. def OAI.Erdos3.prescribedCRTCofactorUnit line 30
  5. theorem OAI.Erdos3.prescribedCRTCofactorUnit_coe line 36
  6. theorem OAI.Erdos3.prescribedCRTCofactor_isUnit line 41
  7. theorem OAI.Erdos3.prescribedCRTProductStep_cast line 46
  8. def OAI.Erdos3.prescribedCRTProductStepEquiv line 51
  9. theorem OAI.Erdos3.prescribedCRTProductStepEquiv_apply line 66
  10. theorem OAI.Erdos3.prescribedCRTProductStepEquiv_local_step line 72
  11. theorem OAI.Erdos3.prescribedCRTProductStepEquiv_symm_local_step line 80
  12. theorem OAI.Erdos3.prescribedCRTPolynomialInput_product_step line 90
  13. theorem OAI.Erdos3.prescribedCRTPolynomialInput_product_step_symm line 108