OAI/NumberTheory/DirichletL/Moments/FirstReferenceSource.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.CenteredMomentFirstReferenceSource.SourceBlocks line 27
2. def OAI.SevenEighths.CenteredMomentFirstReferenceSource.originalBlock line 32
3. def OAI.SevenEighths.CenteredMomentFirstReferenceSource.radicalWeight line 45
4. lemma OAI.SevenEighths.CenteredMomentFirstReferenceSource.radicalWeight_nonneg line 51
5. lemma OAI.SevenEighths.CenteredMomentFirstReferenceSource.physicalMass_eq_sum line 55
6. theorem OAI.SevenEighths.CenteredMomentFirstReferenceSource.original_block_sum line 62