Theorem continuous_linear_map.has_sum_of_summable
Modification history
2020-10-13 23:51
src/analysis/normed_space/operator_norm.lean
feat(analysis/normed_space): unconditionally convergent series in `R^n` is absolutely convergent (#4551)
Deleted continuous_linear_map.has_sum_of_summableView on Github →