OAI/NumberTheory/DirichletL/Eisenstein/RamifiedNormWeights.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.predicateFiberEquiv line 79
  2. def OAI.CubicEisenstein.predicateKernelEquiv line 90
  3. lemma OAI.CubicEisenstein.card_ring_eq_card_mul_kernel line 97
  4. lemma OAI.CubicEisenstein.card_units_eq_card_mul_kernel line 103
  5. lemma OAI.CubicEisenstein.card_units_mul_card_target line 115
  6. theorem OAI.CubicEisenstein.idealTotient_pow_succ line 122
  7. theorem OAI.CubicEisenstein.idealTotient_cube line 140
  8. def OAI.CubicEisenstein.unitsRingEquiv line 144
  9. theorem OAI.CubicEisenstein.idealTotient_mul line 149
  10. theorem OAI.CubicEisenstein.card_admissible_cube_product line 158
  11. lemma OAI.CubicEisenstein.isUnit_quotient_iff_sup line 170
  12. lemma OAI.CubicEisenstein.residue_unit_mobius line 194
  13. lemma OAI.CubicEisenstein.sum_indicator_const line 215
  14. lemma OAI.CubicEisenstein.card_quotient_multiples line 220
  15. theorem OAI.CubicEisenstein.idealTotient_moebius line 244
  16. def OAI.CubicEisenstein.unramifiedNormWeight line 280
  17. lemma OAI.CubicEisenstein.unramifiedNormWeight_of_good line 293
  18. lemma OAI.CubicEisenstein.unramifiedNormWeight_of_bad line 296
  19. lemma OAI.CubicEisenstein.primaryGenerator_injective_good line 299
  20. lemma OAI.CubicEisenstein.norm_unramifiedNormWeight line 306
  21. theorem OAI.CubicEisenstein.unramifiedNormWeight_summable_norm line 321
  22. lemma OAI.CubicEisenstein.norm_ideal_moebius_le_one line 335
  23. lemma OAI.CubicEisenstein.moebius_unramifiedNormWeight_summable_norm line 340
  24. def OAI.CubicEisenstein.unramifiedIdealZeta line 347
  25. def OAI.CubicEisenstein.unramifiedMobiusSeries line 349
  26. theorem OAI.CubicEisenstein.unramifiedMobiusSeries_mul_zeta line 357
  27. theorem OAI.CubicEisenstein.unramifiedIdealZeta_ne_zero line 401
  28. theorem OAI.CubicEisenstein.unramifiedMobiusSeries_eq_inv line 407
  29. lemma OAI.CubicEisenstein.unramifiedNormWeight_shift line 415
  30. lemma OAI.CubicEisenstein.mulFiber_totient_sum line 424
  31. def OAI.CubicEisenstein.unramifiedTotientSeries line 459
  32. theorem OAI.CubicEisenstein.unramifiedTotientSeries_product line 462
  33. theorem OAI.CubicEisenstein.unramifiedTotientSeries_quotient line 500
  34. lemma OAI.CubicEisenstein.idealTotient_le_absNorm line 505
  35. theorem OAI.CubicEisenstein.unramifiedTotientSeries_summable_norm line 511
  36. theorem OAI.CanonicalQuadraticSieve.originalPairLow_squarefree_tsum line 530
  37. theorem OAI.CanonicalQuadraticSieve.idealZeroMask_span_eq line 598
  38. theorem OAI.CanonicalQuadraticSieve.idealZeroMask_mul line 609
  39. theorem OAI.CanonicalQuadraticSieve.jointMask_generator line 621
  40. theorem OAI.CanonicalQuadraticSieve.jointMask_zero line 632