OAI/NumberTheory/DirichletL/Moments/CommonProfile.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentCommonProfile.liveIndices line 15
2. def OAI.SevenEighths.CenteredMomentCommonProfile.remainingTuple line 17
3. theorem OAI.SevenEighths.CenteredMomentCommonProfile.remainingTuple_slot line 20
4. theorem OAI.SevenEighths.CenteredMomentCommonProfile.remainingTuple_plain line 23
5. theorem OAI.SevenEighths.CenteredMomentCommonProfile.remaining_product line 26
6. theorem OAI.SevenEighths.CenteredMomentCommonProfile.slot_profiles_split line 40
7. theorem OAI.SevenEighths.CenteredMomentCommonProfile.profile_common_allocation line 57
8. theorem OAI.SevenEighths.CenteredMomentCommonProfile.actual_frozen_slots line 83