Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-30 14:07 8fa8f175

View on Github →

refactor(tsum): use ∑' instead of ∑ as notation (#2571) As discussed in: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/big.20ops/near/195821357 This is the result of

git grep -l '∑' | grep -v "mean_ineq" | xargs sed -i "s/∑/∑'/g"

after manually cleaning some occurences of ∑ in TeX strings. Probably ∑ has now also been changed in a lot of comments and docstrings, but my reasoning is that if the string "tsum" occurs in the file, then it doesn't do harm to write ∑' instead of ∑ in the comments as well.

Estimated changes

modified theorem norm_tsum_le_tsum_norm
modified theorem ennreal.tsum_geometric
modified theorem tsum_geometric
modified theorem tsum_geometric_nnreal
modified theorem tsum_geometric_two'
modified theorem tsum_geometric_two
modified theorem pmf.bind_apply
modified theorem pmf.tsum_coe
modified theorem summable.has_sum
modified theorem summable.has_sum_iff
modified theorem tsum_add
modified theorem tsum_eq_has_sum
modified theorem tsum_eq_zero_add
modified theorem tsum_equiv
modified theorem tsum_fintype
modified theorem tsum_ite_eq
modified theorem tsum_le_tsum
modified theorem tsum_mul_left
modified theorem tsum_mul_right
modified theorem tsum_neg
modified theorem tsum_nonneg
modified theorem tsum_nonpos
modified theorem tsum_sub
modified theorem tsum_zero
modified theorem nnreal.coe_tsum