OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/DualSmoothZeroLeft.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.dual_smooth_zero_left line 26
2. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.dual_smooth_zero_right line 34
3. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.sum_range_eq_Ioc line 42
4. def OAI.OrdinaryCorrelations.SourcePrimeFactor.dualTwist line 62
5. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.dualTwist_bound line 65
6. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.actual_short_prime_decomposition line 71