OAI/Combinatorics/Progressions/Fourier/RationalCharacterIndividualModulus.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.rationalCharacterIndividualModulus line 13
  2. theorem OAI.Erdos3.rationalCharacterIndividualModulus_dvd line 16
  3. theorem OAI.Erdos3.rationalCharacterIndividualModulus_test_dvd line 21
  4. theorem OAI.Erdos3.rationalCharacterIndividualModulus_order_dvd line 25
  5. theorem OAI.Erdos3.rationalCharacterIndividualModulus_pos line 31
  6. instance OAI.Erdos3.rationalCharacterIndividualModulus_neZero line 35
  7. theorem OAI.Erdos3.rationalCharacterIndividualModulus_le_mul line 39
  8. theorem OAI.Erdos3.exists_rationalCharacterIndividualReduction line 47
  9. def OAI.Erdos3.rationalCharacterIndividualReduction line 54
  10. theorem OAI.Erdos3.rationalCharacterIndividualReduction_order line 58
  11. theorem OAI.Erdos3.rationalCharacterIndividualReduction_apply line 62
  12. theorem OAI.Erdos3.rationalCharacterIndividualReduction_intCast line 68
  13. theorem OAI.Erdos3.rationalCharacterIndividualModulus_reduce_test line 82
  14. theorem OAI.Erdos3.rationalCharacterIndividualReduction_phase_uniform line 93
  15. theorem OAI.Erdos3.rationalCharacterIndividualReduction_uniform line 109
  16. theorem OAI.Erdos3.rationalCharacterIndividualReduction_star_uniform line 117
  17. theorem OAI.Erdos3.rationalCharacterIndividualReduction_partial_phase_uniform line 130
  18. theorem OAI.Erdos3.rationalCharacterIndividualReduction_partial_star_uniform line 159