OAI/NumberTheory/DirichletL/Moments/FirstPhysicalSource.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentFirstPhysicalSource.columns line 22
  2. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalSource.column_supported line 25
  3. def OAI.SevenEighths.CenteredMomentFirstPhysicalSource.element line 29
  4. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalSource.element_span line 32
  5. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalSource.element_supported line 35
  6. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalSource.element_primary line 39
  7. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalSource.active_span_dvd line 44
  8. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalSource.element_coprime_active line 50
  9. def OAI.SevenEighths.CenteredMomentFirstPhysicalSource.coefficient line 56
  10. def OAI.SevenEighths.CenteredMomentFirstPhysicalSource.inactiveWeight line 59
  11. def OAI.SevenEighths.CenteredMomentFirstPhysicalSource.block line 62
  12. def OAI.SevenEighths.CenteredMomentFirstPhysicalSource.scalar line 87
  13. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalSource.block_eq_whole line 94