Theorem Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpow

Modification history

2025-02-09 19:16
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 2) (#20660) …
Modified Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpowView on Github →
2025-01-27 10:18
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) …
Added Asymptotics.IsBigO.mul_atTop_rpow_of_isBigO_rpowView on Github →