OAI/NumberTheory/DirichletL/Moments/CommonRadialData.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.CenteredMomentCommonRadialData.Input line 19
2. def OAI.SevenEighths.CenteredMomentCommonRadialData.Input.pools line 34
3. lemma OAI.SevenEighths.CenteredMomentCommonRadialData.Input.pools_ne line 38
4. lemma OAI.SevenEighths.CenteredMomentCommonRadialData.Input.slot_support line 47
5. lemma OAI.SevenEighths.CenteredMomentCommonRadialData.alloc_ne line 51
6. lemma OAI.SevenEighths.CenteredMomentCommonRadialData.alloc_norm_pos line 56
7. def OAI.SevenEighths.CenteredMomentCommonRadialData.commonData line 60
8. lemma OAI.SevenEighths.CenteredMomentCommonRadialData.common_profile_le line 98