Theorem Asymptotics.IsTheta.summable_iff_nat

Modification history

2026-02-24 22:57
Mathlib/Analysis/Normed/Module/FiniteDimension.lean
feat(Analysis/Normed/Module/FiniteDimension): add lemmas on IsTheta and summability (#34914) …
Added Asymptotics.IsTheta.summable_iff_natView on Github →