Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-12 19:31 c1894c88

View on Github →

chore(analysis|measure_theory|topology): give tsum notation precedence 67 (#5709) This saves us a lot of () In particular, lean no longer thinks that ∑' i, f i = 37 is a tsum of propositions.

Estimated changes

modified theorem ennreal.tsum_geometric
modified theorem tsum_geometric_nnreal
modified theorem tsum_geometric_of_abs_lt_1
modified theorem tsum_geometric_of_lt_1
modified theorem tsum_geometric_of_norm_lt_1
modified theorem tsum_geometric_two'
modified theorem tsum_geometric_two
modified theorem pmf.bind_apply
modified theorem pmf.tsum_coe
modified theorem equiv.tsum_eq
modified theorem has_sum.tsum_eq
modified theorem summable.has_sum_iff
modified theorem summable.tsum_mul_left
modified theorem tsum_add
modified theorem tsum_eq_zero_iff
modified theorem tsum_fintype
modified theorem tsum_ite_eq
modified theorem tsum_le_tsum
modified theorem tsum_neg
modified theorem tsum_nonneg
modified theorem tsum_nonpos
modified theorem tsum_smul
modified theorem tsum_sub
modified theorem tsum_zero
modified theorem ennreal.tendsto_sum_nat_add
modified theorem ennreal.tsum_sub
modified theorem nnreal.coe_tsum
modified theorem nnreal.tsum_mul_left