OAI/NumberTheory/DirichletL/Moments/CommonSupport.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.CenteredMomentCommonSupport.Residue line 12
  2. def OAI.SevenEighths.CenteredMomentCommonSupport.principalCRT line 14
  3. theorem OAI.SevenEighths.CenteredMomentCommonSupport.principalCRT_mk line 20
  4. lemma OAI.SevenEighths.CenteredMomentCommonSupport.coprime_mul_dvd_iff line 25
  5. theorem OAI.SevenEighths.CenteredMomentCommonSupport.full_product_congruence line 33
  6. theorem OAI.SevenEighths.CenteredMomentCommonSupport.isUnit_residue_of_coprime line 39
  7. lemma OAI.SevenEighths.CenteredMomentCommonSupport.residue_eq_zero_iff_dvd line 48
  8. theorem OAI.SevenEighths.CenteredMomentCommonSupport.full_congruence_split line 52
  9. theorem OAI.SevenEighths.CenteredMomentCommonSupport.sum_residual_constraints line 72
  10. theorem OAI.SevenEighths.CenteredMomentCommonSupport.fullCorrelation_unit_change line 108
  11. lemma OAI.SevenEighths.CenteredMomentCommonSupport.character_unit_inverse line 133
  12. def OAI.SevenEighths.CenteredMomentCommonSupport.residueUnit line 137
  13. theorem OAI.SevenEighths.CenteredMomentCommonSupport.residueUnit_coe line 140
  14. def OAI.SevenEighths.CenteredMomentCommonSupport.scaledCommonCorrelation line 144
  15. theorem OAI.SevenEighths.CenteredMomentCommonSupport.scaledCommonCorrelation_eq line 152
  16. theorem OAI.SevenEighths.CenteredMomentCommonSupport.fullModulusCorrelation_extract line 165
  17. theorem OAI.SevenEighths.CenteredMomentCommonSupport.fullModulusCorrelation_complete_support line 212