OAI/NumberTheory/DirichletL/Moments/FirstCommonFourierTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentFirstCommonFourierTransport.quotient_function_heq line 16
2. def OAI.SevenEighths.CenteredMomentFirstCommonFourierTransport.retainedFourierTerm line 26
3. theorem OAI.SevenEighths.CenteredMomentFirstCommonFourierTransport.retainedFourierTerm_transport line 35
4. def OAI.SevenEighths.CenteredMomentFirstCommonFourierTransport.fixedRetainedTerm line 46
5. theorem OAI.SevenEighths.CenteredMomentFirstCommonFourierTransport.canonicalRetainedTerm_fixed line 55
6. def OAI.SevenEighths.CenteredMomentFirstCommonFourierTransport.inactiveEquiv line 77
7. theorem OAI.SevenEighths.CenteredMomentFirstCommonFourierTransport.inactiveEquiv_val line 82
8. theorem OAI.SevenEighths.CenteredMomentFirstCommonFourierTransport.canonicalRetainedPair_fixed line 86