OAI/NumberTheory/DirichletL/Hecke/LocalEulerIdentities.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortDraftHeckeBridge.chiMinusThree_mod_one line 37
  2. theorem OAI.ShortDraftHeckeBridge.chiMinusThree_mod_two line 47
  3. theorem OAI.ShortDraftHeckeBridge.chiMinusThree_mod_zero line 58
  4. theorem OAI.ShortDraftHeckeBridge.invCharAF_prime_pow_ge_two line 68
  5. theorem OAI.ShortDraftHeckeBridge.pairAF_prime_pow_ge_three line 75
  6. instance OAI.ShortDraftHeckeBridge.(instance at line 98) line 98
  7. theorem OAI.ShortDraftHeckeBridge.base_ring_rank_two line 101
  8. theorem OAI.ShortDraftHeckeBridge.baseChangeWeight_zero_of_norm_prime_pow_ge_three line 106
  9. theorem OAI.ShortDraftHeckeBridge.normFiberCoeff_baseChangeWeight_prime_pow_ge_three line 129
  10. theorem OAI.ShortDraftHeckeBridge.normFiberCoeff_eq_pairAF_prime_pow_ge_three line 139
  11. theorem OAI.ShortDraftHeckeBridge.char_prime_zero_of_dvd_level line 146
  12. theorem OAI.ShortDraftHeckeBridge.baseChangeChar_prime_zero_of_dvd_q line 156
  13. theorem OAI.NormSplitArithmetic.eq_parts_of_coprime_square_bounds line 166
  14. abbrev OAI.NormFiberCRT.O line 195
  15. abbrev OAI.NormFiberCRT.K line 196
  16. instance OAI.NormFiberCRT.(instance at line 198) line 198
  17. theorem OAI.NormFiberCRT.ring_rank_two line 201
  18. theorem OAI.NormFiberCRT.ideal_eq_factors line 206
  19. theorem OAI.NormFiberCRT.ideal_factor_norms line 234
  20. abbrev OAI.NormFiberMult.O line 256
  21. theorem OAI.NormFiberMult.ideal_sup_span_norm_left line 258
  22. theorem OAI.NormFiberMult.ideal_sup_span_norm_right line 289
  23. theorem OAI.NormFiberMult.weighted_norm_fiber_mul line 296
  24. theorem OAI.ShortDraftHeckeBridge.baseChange_normFiber_mul line 357
  25. theorem OAI.ShortDraftHeckeBridge.normFiberCoeff_baseChangeWeight_one line 365
  26. theorem OAI.ShortDraftHeckeBridge.baseChange_normFiber_isMultiplicative line 376
  27. theorem OAI.ShortDraftHeckeBridge.baseChangeChar_prime_apply line 389
  28. theorem OAI.ShortDraftHeckeBridge.normFiberCoeff_eq_pairAF_prime line 411
  29. theorem OAI.ShortDraftHeckeBridge.normFiberCoeff_eq_pairAF_prime_sq line 435
  30. theorem OAI.ShortDraftHeckeBridge.normFiberCoeff_eq_pairInverseCoeff_of_local line 464
  31. theorem OAI.ShortDraftHeckeBridge.normFiberCoeff_baseChange_eq_pairInverseCoeff line 491
  32. theorem OAI.ShortDraftHeckeBridge.dirichletTarget_of_normFiber_exp_bound line 500
  33. theorem OAI.ShortDraftHeckeBridge.rpow_le_one_add_of_exponent_Icc line 516
  34. theorem OAI.ShortDraftHeckeBridge.tsum_add_one_mul_geometric line 524
  35. theorem OAI.ShortDraftHeckeBridge.summable_add_one_mul_geometric line 530
  36. theorem OAI.ShortDraftHeckeBridge.geometric_rpow_moment_bound line 536
  37. def OAI.ShortDraftHeckeBridge.prefixCoeff line 594
  38. theorem OAI.ShortDraftHeckeBridge.tsum_eq_one_sub_mul_tsum_prefix line 597
  39. theorem OAI.ShortDraftHeckeBridge.exp_inv_geometric_gap line 634
  40. theorem OAI.ShortDraftHeckeBridge.normFiberExpSum_le_of_prefix_power line 663
  41. theorem OAI.ShortDraftHeckeBridge.normFiberExpSum_isBigO_of_prefix_power line 735