Commit 2022-05-08 18:01 163ef61e

View on Github →

feat(topology/algebra/infinite_sum): add tsum_star (#13999) These lemmas names are copied from tsum_neg and friends. As a result, star_exp can be golfed and generalized.

Estimated changes

Modified src/analysis/normed_space/exponential.lean

modified theorem star_exp

Modified src/analysis/normed_space/star/exponential.lean

Modified src/topology/algebra/infinite_sum.lean

added theorem has_sum.star

added theorem summable.of_star

added theorem summable.star

added theorem summable_star_iff'

added theorem summable_star_iff

added theorem tsum_star