Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-07 20:04 b9689bdc

View on Github →

feat(topology/algebra/infinite_sum): add lemmas about continuous linear maps (#5243)

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_equiv.tsum_eq_iff

Modified src/topology/algebra/infinite_sum.lean

added theorem has_sum.smul

added theorem summable.smul

added theorem tsum_smul