OAI/NumberTheory/DirichletL/ChineseRemainder/AdditiveCharacters.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortDraftCRT.addChar_crt_pair line 19
  2. theorem OAI.ShortDraftCRT.addChar_crt_of_isCoprime line 29
  3. theorem OAI.ShortDraftCRT.bezout_with_lam_cube line 42
  4. theorem OAI.ShortDraftCRT.normalized_crt_pair line 56
  5. theorem OAI.ShortDraftCRT.coprime_cross_numerator line 76
  6. def OAI.ShortDraftCRT.crossDen line 93
  7. def OAI.ShortDraftCRT.crossNum line 97
  8. def OAI.ShortDraftCRT.GoodRows line 101
  9. theorem OAI.ShortDraftCRT.coprime_cross_num_list line 106
  10. theorem OAI.ShortDraftCRT.crossDen_ne_zero line 122
  11. theorem OAI.ShortDraftCRT.crossDen_eq_product line 140
  12. theorem OAI.ShortDraftCRT.crossNum_mod_head line 149
  13. theorem OAI.ShortDraftCRT.product_coprime_of_each line 155
  14. theorem OAI.ShortDraftCRT.goodRows_of_pairwise line 168
  15. theorem OAI.ShortDraftCRT.cross_fraction_eq line 193
  16. theorem OAI.ShortDraftCRT.fixed_ray_denominator line 226
  17. theorem OAI.ShortDraftCRT.local_epsilon_identity line 237
  18. theorem OAI.ShortDraftCRT.addChar_congr_of_dvd line 243
  19. theorem OAI.ShortDraftCRT.list_prod_coprime_right line 263
  20. theorem OAI.ShortDraftCRT.list_prod_ne_zero line 272
  21. theorem OAI.ShortDraftCRT.addChar_crt_list_codifferent line 281
  22. theorem OAI.ShortDraftDescent.binary_energy_descent line 344
  23. theorem OAI.ShortDraftDescent.contraction_terminates_after_3001 line 397
  24. lemma OAI.ShortDraftTrace.lam_ne_zero line 445
  25. lemma OAI.ShortDraftTrace.conj_lam line 451
  26. lemma OAI.ShortDraftTrace.omega_sub_square line 456
  27. theorem OAI.ShortDraftTrace.trace_div_lam line 459
  28. theorem OAI.ShortDraftTrace.trace_character_period line 471
  29. def OAI.ShortDraftTrace.ω₃ line 483
  30. theorem OAI.ShortDraftTrace.omega_sq line 485
  31. theorem OAI.ShortDraftTrace.omega_conj line 497
  32. theorem OAI.ShortDraftTrace.eisenstein_trace_period line 504
  33. def OAI.ShortDraftTrace.breveE line 512
  34. theorem OAI.ShortDraftTrace.breveE_period_lam line 523
  35. theorem OAI.ShortDraftTrace.breveE_period_integer line 527
  36. theorem OAI.ShortDraftTrace.lam_eq_sqrt3_mul_I line 544
  37. theorem OAI.ShortDraftTrace.sub_conj_eq line 549
  38. theorem OAI.ShortDraftTrace.breveE_div_lam_eq_e line 556
  39. def OAI.ShortDraftTrace.eisensteinSubring line 573
  40. def OAI.ShortDraftTrace.lamEis line 593
  41. theorem OAI.ShortDraftTrace.breveE_period_eisenstein line 596