Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-05 22:38 f80ae1f8

View on Github →

feat(topology/infinite_sum): add tsum (with ∑ notation) and has_sum; add lemmas for different algebraic structures

Estimated changes

modified theorem continuous_const
deleted theorem exists_is_sum_of_is_sum
added def has_sum
added theorem has_sum_add
added theorem has_sum_mul_left
added theorem has_sum_mul_right
added theorem has_sum_neg
added theorem has_sum_spec
added theorem has_sum_sub
added theorem has_sum_sum
added theorem has_sum_zero
modified theorem is_sum_hom
added theorem is_sum_mul_left
added theorem is_sum_mul_right
added theorem is_sum_neg
added theorem is_sum_sub
deleted theorem is_sum_sum_of_ne_zero
added theorem is_sum_tsum
added theorem is_sum_unique
added def tsum
added theorem tsum_add
added theorem tsum_eq_is_sum
added theorem tsum_mul_left
added theorem tsum_mul_right
added theorem tsum_neg
added theorem tsum_sub
added theorem tsum_sum
added theorem tsum_zero
modified theorem continuous_mul
modified theorem tendsto_mul