OAI/NumberTheory/DirichletL/Moments/CRT.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.CenteredMomentCorrelation.fullCorrelation_ringEquivline 12 - theorem
OAI.SevenEighths.CenteredMomentCorrelation.fullCorrelation_productline 25 - theorem
OAI.SevenEighths.CenteredMomentCorrelation.fullCorrelation_piline 55 - theorem
OAI.SevenEighths.CenteredMomentCorrelation.fullCorrelation_idealCRTline 86 - def
OAI.SevenEighths.CenteredMomentCorrelation.crtCharacterline 100 - theorem
OAI.SevenEighths.CenteredMomentCorrelation.crtCharacter_applyline 116