Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-05 19:24 7d8e3f3a

View on Github →

feat(algebra): add ordered (non-cancellative) additive monoid; use for sum-big operator

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.sum_eq_zero_iff_of_nonneg

added theorem finset.sum_le_sum'

added theorem finset.sum_le_sum_of_ne_zero

added theorem finset.sum_le_sum_of_subset

added theorem finset.sum_le_sum_of_subset_of_nonneg

added theorem finset.sum_le_zero'

added theorem finset.zero_le_sum'

Created algebra/ordered_monoid.lean

added theorem add_eq_zero_iff

added theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg'

added theorem add_le_add'

added theorem add_le_add_left'

added theorem add_le_add_right'

added theorem add_le_of_le_of_nonpos'

added theorem add_le_of_nonpos_of_le'

added theorem add_lt_of_lt_of_neg'

added theorem add_lt_of_lt_of_nonpos'

added theorem add_lt_of_neg_of_lt'

added theorem add_lt_of_nonpos_of_lt'

added theorem add_neg'

added theorem add_neg_of_neg_of_nonpos'

added theorem add_neg_of_nonpos_of_neg'

added theorem add_nonneg'

added theorem add_nonpos'

added theorem add_pos'

added theorem add_pos_of_nonneg_of_pos'

added theorem add_pos_of_pos_of_nonneg'

added theorem le_add_of_le_of_nonneg'

added theorem le_add_of_nonneg_left'

added theorem le_add_of_nonneg_of_le'

added theorem le_add_of_nonneg_right'

added theorem le_iff_exists_add

added theorem lt_add_of_lt_of_nonneg'

added theorem lt_add_of_lt_of_pos'

added theorem lt_add_of_nonneg_of_lt'

added theorem lt_add_of_pos_of_lt'

added theorem lt_of_add_lt_add_left'

added theorem lt_of_add_lt_add_right'

added theorem zero_le