OAI/NumberTheory/DirichletL/Arithmetic/IdealMobius.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IdealMobiusDivisorSum.O line 74
  2. def OAI.IdealMobiusDivisorSum.idealDivisors line 76
  3. theorem OAI.IdealMobiusDivisorSum.mem_idealDivisors line 80
  4. def OAI.IdealMobiusDivisorSum.primeSupport line 90
  5. theorem OAI.IdealMobiusDivisorSum.support_prime line 92
  6. theorem OAI.IdealMobiusDivisorSum.support_product_ne_zero line 95
  7. theorem OAI.IdealMobiusDivisorSum.factors_support_product line 99
  8. theorem OAI.IdealMobiusDivisorSum.squarefree_support_product line 104
  9. theorem OAI.IdealMobiusDivisorSum.support_product_dvd line 110
  10. theorem OAI.IdealMobiusDivisorSum.moebius_support_product line 118
  11. theorem OAI.IdealMobiusDivisorSum.support_product_injective line 125
  12. theorem OAI.IdealMobiusDivisorSum.squarefree_divisor_support line 132
  13. theorem OAI.IdealMobiusDivisorSum.squarefree_support_product_self line 138
  14. theorem OAI.IdealMobiusDivisorSum.squarefree_divisors_eq_image line 149
  15. theorem OAI.IdealMobiusDivisorSum.primeSupport_empty_iff line 161
  16. theorem OAI.IdealMobiusDivisorSum.sum_moebius_divisors line 175
  17. abbrev OAI.CompletedGauss.O line 202
  18. def OAI.CompletedGauss.primaryPrime line 205
  19. theorem OAI.CompletedGauss.primaryPrime_spec line 211
  20. theorem OAI.CompletedGauss.primaryPrime_ne_zero line 221
  21. def OAI.CompletedGauss.primaryGenerator line 232
  22. theorem OAI.CompletedGauss.primaryGenerator_zero line 235
  23. theorem OAI.CompletedGauss.primaryGenerator_bot line 237
  24. theorem OAI.CompletedGauss.primaryGenerator_one line 239
  25. theorem OAI.CompletedGauss.primaryGenerator_mul line 243
  26. def OAI.CompletedGauss.primaryGeneratorHom line 253
  27. theorem OAI.CompletedGauss.primaryGenerator_ne_zero_ideal line 259
  28. theorem OAI.CompletedGauss.primaryPrime_factor_ne_zero line 263
  29. theorem OAI.CompletedGauss.span_multiset_prod line 271
  30. theorem OAI.CompletedGauss.primaryGenerator_spec line 278
  31. theorem OAI.CompletedGauss.primaryGenerator_span line 303
  32. theorem OAI.CompletedGauss.primaryGenerator_norm_sq line 321
  33. theorem OAI.CompletedGauss.compact_window_bound line 327
  34. theorem OAI.CompletedGauss.norm_at_least_one line 334
  35. theorem OAI.CompletedGauss.triple_scale_bounds line 338
  36. theorem OAI.CompletedGauss.finite_support_norm_triple line 356
  37. def OAI.CompletedGauss.primeSupport line 388
  38. abbrev OAI.CompletedGauss.PrimeIndex line 391
  39. instance OAI.CompletedGauss.primeIndexMaximal line 393
  40. theorem OAI.CompletedGauss.primeIndex_good line 398
  41. theorem OAI.CompletedGauss.primeIndex_le line 403
  42. def OAI.CompletedGauss.cubicRow line 406
  43. def OAI.CompletedGauss.gaussTwo line 411
  44. def OAI.CompletedGauss.squarefreeGaussCoefficient line 419
  45. theorem OAI.CompletedGauss.squarefreeGaussCoefficient_zero line 424
  46. theorem OAI.CompletedGauss.squarefreeGaussCoefficient_bot line 427
  47. theorem OAI.CompletedGauss.squarefreeGaussCoefficient_eq line 430
  48. theorem OAI.CompletedGauss.angularFactor_mul line 436
  49. def OAI.CompletedGauss.cubeWeight line 442
  50. theorem OAI.CompletedGauss.cubeWeight_zero line 452
  51. theorem OAI.CompletedGauss.cubeWeight_bot line 455
  52. def OAI.CompletedGauss.columnWeight line 457
  53. theorem OAI.CompletedGauss.columnWeight_zero line 460
  54. theorem OAI.CompletedGauss.columnWeight_bot line 463
  55. def OAI.CompletedGauss.Vstar line 465
  56. def OAI.CompletedGauss.summand line 467
  57. def OAI.CompletedGauss.completedT line 471
  58. theorem OAI.CompletedGauss.summand_zero_left line 474
  59. theorem OAI.CompletedGauss.summand_zero_right line 477
  60. theorem OAI.CompletedGauss.summand_zero_window line 480
  61. theorem OAI.CompletedGauss.cubicRow_mk line 484
  62. theorem OAI.CompletedGauss.cubicRow_zero_iff line 490
  63. theorem OAI.CompletedGauss.primaryGenerator_norm line 505
  64. theorem OAI.CompletedGauss.cubeWeight_span line 509
  65. theorem OAI.CompletedGauss.columnWeight_eq line 518
  66. theorem OAI.CompletedGauss.columnWeight_zero_of_mask line 524
  67. theorem OAI.CompletedGauss.cubeWeight_zero_of_mask line 528
  68. def OAI.CompletedGauss.MulFiber line 538
  69. def OAI.CompletedGauss.mulFiberDivisorEquiv line 540
  70. theorem OAI.CompletedGauss.mulFiber_moebius_sum line 561
  71. theorem OAI.CompletedGauss.ideal_cube_convolution line 576