Theorem summable_powerSeries_of_norm_lt_one

Modification history

2024-02-01 01:58
Mathlib/Analysis/SpecificLimits/Normed.lean
feat: absolute convergence from conditional of power series (#9955) …
Added summable_powerSeries_of_norm_lt_oneView on Github →