OAI/NumberTheory/DirichletL/Moments/CompleteCommon.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentCompleteCommon.commonSupport line 14
  2. def OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart line 16
  3. def OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart line 19
  4. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonSupport_comm line 22
  5. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.supportExtract_eq_power_product line 25
  6. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.supportResidual_eq_power_product line 38
  7. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_eq_supportExtract line 51
  8. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_eq_supportResidual line 56
  9. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_ne_zero line 66
  10. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_ne_zero line 70
  11. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.reconstruct line 74
  12. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_support line 79
  13. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonParts_equal_support line 84
  14. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_support line 88
  15. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_valuation line 95
  16. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_valuation line 100
  17. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_residualPart_coprime line 105
  18. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_own_residual_coprime line 110
  19. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonProduct_leftResidual_coprime line 115
  20. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonProduct_rightResidual_coprime line 119
  21. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualParts_coprime line 123
  22. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.canonical_complete_extraction line 128
  23. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_dvd line 148
  24. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_dvd line 151
  25. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_original_coprime line 154
  26. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_eq_one_of_empty line 159
  27. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_eq_of_empty line 162
  28. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonSupport_empty_iff line 168
  29. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_one_right line 174
  30. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_one_left line 178
  31. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_one_right line 182
  32. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_one_left line 186
  33. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.extracted_commonRadical line 189
  34. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonRadical_dvd_commonPart line 195
  35. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.squarefree_mask_survives line 200
  36. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_supported line 214
  37. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_supported line 218
  38. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.primaryGenerator_reconstruct line 222
  39. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.primary_complete_extraction line 228
  40. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.common_valuations_pos line 260
  41. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.residualPart_self line 266
  42. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.commonPart_self line 269
  43. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.absNorm_reconstruct line 274
  44. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.absNorm_commonPart_le line 279
  45. theorem OAI.SevenEighths.CenteredMomentCompleteCommon.absNorm_residualPart_le line 284