Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-05 15:01 de832056

View on Github →

refactor(algebra/big_operators) delete duplicates and change names (#1301)

refactor(algebra/big_operators) delete duplicates and change names
fix build

Estimated changes

Modified src/algebra/big_operators.lean

deleted theorem finset.sum_le_sum'

deleted theorem finset.sum_le_zero'

deleted theorem finset.sum_le_zero

added theorem finset.sum_nonneg

added theorem finset.sum_nonpos

deleted theorem finset.zero_le_sum'

deleted theorem finset.zero_le_sum

Modified src/analysis/convex.lean

Modified src/analysis/normed_space/basic.lean

Modified src/data/complex/exponential.lean

Modified src/data/real/ennreal.lean

Modified src/measure_theory/integration.lean

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/instances/ennreal.lean