Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-10 09:47 836c0a26

View on Github →

chore(*): use sum notation (#3014) The biggest field test of the new summation notation.

Estimated changes

modified theorem finset.exists_le_of_sum_le
modified theorem convex.sum_mem
modified theorem finset.center_mass_insert
modified theorem nnreal.am_gm_weighted
modified theorem nnreal.pow_am_le_am_pow
modified theorem nnnorm_sum_le
modified theorem norm_sum_le
modified theorem composition.sum_blocks_fun
modified def complex.exp'
modified theorem complex.exp_sum
modified theorem complex.is_cau_exp
modified theorem is_cau_geo_series_const
modified theorem is_cau_series_of_abv_cau
modified theorem real.exp_sum
modified theorem nat.sum_totient
modified theorem matrix.trace_diag
modified def pmf.of_fintype
modified def has_sum
modified theorem has_sum_fintype
modified theorem tsum_fintype