OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/DyadicCofactorMellin.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SourcePrimeFactor.dyadicCofactorMellin line 23
2. def OAI.SourcePrimeFactor.primeMellin line 29
3. lemma OAI.SourcePrimeFactor.prime_coefficient_norm line 33
4. lemma OAI.SourcePrimeFactor.norm_primeMellin line 40
5. lemma OAI.SourcePrimeFactor.dyadicCofactorMellin_eq line 50
6. theorem OAI.SourcePrimeFactor.terminal_cofactor_sparse line 61
7. theorem OAI.SourcePrimeFactor.terminal_product_sparse line 83