OAI/NumberTheory/CubicGauss/DivisorWeights.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Squarefree divisors and Möbius-weighted coprimality decompositions.

  1. lemma OAI.CubicFirstMoment.primary_prime_prod_coprime line 15
  2. lemma OAI.CubicFirstMoment.primary_prime_prod_dvd_iff line 25
  3. lemma OAI.CubicFirstMoment.common_squarefree_split line 33
  4. lemma OAI.CubicFirstMoment.coprime_indicator_prod line 67
  5. lemma OAI.CubicFirstMoment.dvd_indicator_prod line 87
  6. theorem OAI.CubicFirstMoment.coprime_indicator_moebius line 97
  7. lemma OAI.CubicFirstMoment.mem_primaryPrimeFactors_iff line 116
  8. def OAI.CubicFirstMoment.primaryDivisors line 127
  9. lemma OAI.CubicFirstMoment.mem_primaryDivisors line 130
  10. lemma OAI.CubicFirstMoment.primaryDivisors_subset_products line 135
  11. lemma OAI.CubicFirstMoment.primaryDivisors_card_le line 146
  12. lemma OAI.CubicFirstMoment.norm_prod_rpow line 151
  13. theorem OAI.CubicFirstMoment.squarefree_divisor_power_bound line 160
  14. lemma OAI.CubicFirstMoment.primary_prime_dvd_prod_iff line 190
  15. lemma OAI.CubicFirstMoment.primaryPrimeFactors_prime_prod line 201
  16. lemma OAI.CubicFirstMoment.primaryDivisors_eq_products line 209
  17. lemma OAI.CubicFirstMoment.sum_primaryDivisors line 220
  18. lemma OAI.CubicFirstMoment.coprime_indicator_divisors line 233
  19. lemma OAI.CubicFirstMoment.coprime_indicator_ball line 239
  20. theorem OAI.CubicFirstMoment.coprime_pair_sum_moebius line 261