OAI/NumberTheory/DirichletL/Descent/ShortReflectedPower.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.InverseMoment.short_harmonic_small_powerline 14 - theorem
OAI.SevenEighths.InverseMoment.canonical_short_completed_power_energyline 38