OAI/NumberTheory/CubicMoment/Angular/AngularFullPrimeConvolution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.fullStructuredAngularPrimeSum line 13
2. lemma OAI.CubicFirstMoment.fullStructuredAngularPrimeSum_eq line 18
3. lemma OAI.CubicFirstMoment.fullStructuredAngularPrimeSum_partition_cutoff line 25
4. lemma OAI.CubicFirstMoment.fullStructuredAngularPrimeSum_eq_existing line 42