OAI/Combinatorics/Progressions/Fourier/PrimePowerCharacterScaling.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finiteCharacter_exponent line 16
  2. theorem OAI.Erdos3.exists_character_order_eq_exponent line 32
  3. def OAI.Erdos3.characterPullback line 46
  4. theorem OAI.Erdos3.characterPullback_order line 52
  5. def OAI.Erdos3.zmodPiReduction line 65
  6. theorem OAI.Erdos3.zmodPiReduction_apply line 69
  7. theorem OAI.Erdos3.zmodPiReduction_surjective line 73
  8. theorem OAI.Erdos3.zmodPiReduction_kernel_nsmul line 79
  9. theorem OAI.Erdos3.zmodPiReduction_kernel_character line 93
  10. theorem OAI.Erdos3.exists_zmodPiReduction_character line 100
  11. theorem OAI.Erdos3.exists_primePower_character_descent line 126
  12. theorem OAI.Erdos3.zmod_character_order_dvd line 146
  13. theorem OAI.Erdos3.zmod_character_order_pos line 156
  14. theorem OAI.Erdos3.exists_characterOrder_descent line 164
  15. theorem OAI.Erdos3.stdAddChar_mul_modulus_ratio line 195
  16. theorem OAI.Erdos3.stdAddChar_primePower_scaling line 209
  17. theorem OAI.Erdos3.stdAddChar_primePower_row_scaling line 215