Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-30 22:10 b207991b

View on Github →

refactor(data/multiset): move multiset, finset, ordered_monoid

Estimated changes

Modified algebra/big_operators.lean

Modified algebra/default.lean

Modified algebra/ordered_group.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

Deleted algebra/ordered_monoid.lean

deleted theorem add_eq_zero_iff

deleted theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg'

deleted theorem add_le_add'

deleted theorem add_le_add_left'

deleted theorem add_le_add_right'

deleted theorem add_le_of_le_of_nonpos'

deleted theorem add_le_of_nonpos_of_le'

deleted theorem add_lt_of_lt_of_neg'

deleted theorem add_lt_of_lt_of_nonpos'

deleted theorem add_lt_of_neg_of_lt'

deleted theorem add_lt_of_nonpos_of_lt'

deleted theorem add_neg'

deleted theorem add_neg_of_neg_of_nonpos'

deleted theorem add_neg_of_nonpos_of_neg'

deleted theorem add_nonneg'

deleted theorem add_nonpos'

deleted theorem add_pos'

deleted theorem add_pos_of_nonneg_of_pos'

deleted theorem add_pos_of_pos_of_nonneg'

deleted theorem le_add_of_le_of_nonneg'

deleted theorem le_add_of_nonneg_left'

deleted theorem le_add_of_nonneg_of_le'

deleted theorem le_add_of_nonneg_right'

deleted theorem le_iff_exists_add

deleted theorem lt_add_of_lt_of_nonneg'

deleted theorem lt_add_of_lt_of_pos'

deleted theorem lt_add_of_nonneg_of_lt'

deleted theorem lt_add_of_pos_of_lt'

deleted theorem lt_of_add_lt_add_left'

deleted theorem lt_of_add_lt_add_right'

deleted theorem zero_le

Modified analysis/ennreal.lean

Modified data/encodable.lean

Renamed data/finset/basic.lean to data/finset.lean

Deleted data/finset/default.lean

Renamed data/finset/fintype.lean to data/fintype.lean

Renamed data/multiset/basic.lean to data/multiset.lean

Modified data/set/finite.lean