Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 09:36 e70e22f2

View on Github →

feat(data/{list, multiset, finset}/range): add range_add (#10706) Adds range_add lemmas

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.range_add

Modified src/data/list/range.lean

added theorem list.range_add

Modified src/data/multiset/range.lean

added theorem multiset.range_add

added theorem multiset.range_add_eq_union

added theorem multiset.range_disjoint_map_add