OAI/NumberTheory/DirichletL/Moments/SourceLiveColumn.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.CenteredMomentSourceLiveColumn.frozenCoefficientline 16 - def
OAI.SevenEighths.CenteredMomentSourceLiveColumn.liveBoxline 22 - def
OAI.SevenEighths.CenteredMomentSourceLiveColumn.liveProfileline 26 - theorem
OAI.SevenEighths.CenteredMomentSourceLiveColumn.residual_source_columnline 34 - theorem
OAI.SevenEighths.CenteredMomentSourceLiveColumn.original_source_columnline 71