Commit 2023-01-17 18:29 008205aa

View on Github →

chore(analysis/normed/field/basic): split (#18195) Split material on infinite sums out of analysis/normed/field/basic into a new file /infinite_sum. This mimics the structure of analysis/normed/group/*, and reduces the imports of the former.

Estimated changes

Modified src/analysis/asymptotics/asymptotics.lean

Modified src/analysis/normed/field/basic.lean

deleted theorem summable.mul_norm

deleted theorem summable.mul_of_nonneg

deleted theorem summable_mul_of_summable_norm

deleted theorem summable_norm_sum_mul_antidiagonal_of_summable_norm

deleted theorem summable_norm_sum_mul_range_of_summable_norm

deleted theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm

deleted theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm

deleted theorem tsum_mul_tsum_of_summable_norm

Created src/analysis/normed/field/infinite_sum.lean

added theorem summable.mul_norm

added theorem summable.mul_of_nonneg

added theorem summable_mul_of_summable_norm

added theorem summable_norm_sum_mul_antidiagonal_of_summable_norm

added theorem summable_norm_sum_mul_range_of_summable_norm

added theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm

added theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm

added theorem tsum_mul_tsum_of_summable_norm

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/exponential.lean