Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-13 23:51 e2dd1c67

View on Github →

feat(analysis/normed_space): unconditionally convergent series in R^n is absolutely convergent (#4551)

Estimated changes

Modified src/analysis/normed_space/basic.lean

deleted theorem has_sum_of_bounded_monoid_hom_of_has_sum

deleted theorem has_sum_of_bounded_monoid_hom_of_summable

Modified src/analysis/normed_space/finite_dimension.lean

added theorem summable_norm_iff

Modified src/analysis/normed_space/operator_norm.lean

deleted theorem continuous_linear_map.has_sum_of_summable

Modified src/analysis/specific_limits.lean

Modified src/data/indicator_function.lean

added theorem set.indicator_eq_zero_or_self

Modified src/topology/algebra/infinite_sum.lean

added theorem summable.of_neg

added theorem summable_abs_iff

added theorem summable_neg_iff

added theorem summable_subtype_and_compl