OAI/NumberTheory/CubicGram/CommonFactors.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Moebius removal of common factors and coprime Gram decomposition.

  1. lemma OAI.CubicFirstMoment.mixedSymbol_remove_common line 17
  2. lemma OAI.CubicFirstMoment.primary_subsets_prod_dvd line 34
  3. theorem OAI.CubicFirstMoment.primary_moebius_coprimality line 46
  4. lemma OAI.CubicFirstMoment.norm_cubicSymbol_le_one line 109
  5. lemma OAI.CubicFirstMoment.summable_gram_restricted line 115
  6. def OAI.CubicFirstMoment.multiplesMap line 134
  7. lemma OAI.CubicFirstMoment.multiplesMap_bijective line 137
  8. lemma OAI.CubicFirstMoment.tsum_dvd_eq_multiples line 146
  9. lemma OAI.CubicFirstMoment.tsum_primary_dvd_eq_multiples line 155
  10. theorem OAI.CubicFirstMoment.primaryCharacterGram_divisor_scale line 170
  11. theorem OAI.CubicFirstMoment.primaryCharacterGram_common_factor line 189
  12. theorem OAI.CubicFirstMoment.primarySquarefree_common_decomposition line 240
  13. theorem OAI.CubicFirstMoment.primaryCharacterGram_common_poisson line 295