OAI/NumberTheory/DirichletL/Moments/MobiusHarmonicMass.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.CenteredMomentMobiusHarmonicMass.shell_massline 15 - theorem
OAI.SevenEighths.CenteredMomentMobiusHarmonicMass.full_mass_subpowerline 33 - theorem
OAI.SevenEighths.CenteredMomentMobiusHarmonicMass.actual_divisorPool_massline 51