Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-08 07:33 c3768cc8

View on Github →

refactor(data/multiset/basic): remove sub lemmas (#9578)

Remove the multiset sub lemmas that are special cases of lemmas in algebra/order/sub
This gives the list of renamings.
Use derive in pnat.factors.

Estimated changes

Modified src/algebra/associated.lean

Modified src/data/finset/basic.lean

Modified src/data/list/perm.lean

Modified src/data/multiset/antidiagonal.lean

Modified src/data/multiset/basic.lean

deleted theorem multiset.add_sub_cancel

deleted theorem multiset.add_sub_cancel_left

deleted theorem multiset.add_sub_of_le

modified theorem multiset.eq_union_left

deleted theorem multiset.le_sub_add

modified theorem multiset.le_union_left

deleted theorem multiset.sub_add'

deleted theorem multiset.sub_add_cancel

deleted theorem multiset.sub_le_self

deleted theorem multiset.sub_le_sub_left

deleted theorem multiset.sub_le_sub_right

Modified src/data/multiset/nodup.lean

Modified src/data/pnat/factors.lean

deleted theorem prime_multiset.add_sub_of_le

Modified src/group_theory/perm/cycle_type.lean