Commit 2024-03-27 12:36 3713a3fe

View on Github →

chore(Data/List): Use Std lemmas (#11711) Make use of Nat-specific lemmas from Std rather than the general ones provided by mathlib. Also reverse the dependency between Multiset.Nodup/Multiset.dedup and Multiset.sum since only the latter needs algebra. Also rename Algebra.BigOperators.Multiset.Abs to Algebra.BigOperators.Multiset.Order and move some lemmas from Algebra.BigOperators.Multiset.Basic to it. The ultimate goal here is to carve out Data, Algebra and Order sublibraries.

Estimated changes

deleted theorem Multiset.dvd_sum
deleted theorem Multiset.le_prod_of_mem
deleted theorem Multiset.pow_card_le_prod
modified theorem Multiset.prod_eq_one
deleted theorem Multiset.prod_eq_zero
deleted theorem Multiset.prod_eq_zero_iff
deleted theorem Multiset.prod_le_pow_card
deleted theorem Multiset.prod_le_prod_map
deleted theorem Multiset.prod_lt_prod'
deleted theorem Multiset.prod_map_le_prod
deleted theorem Multiset.prod_map_neg
deleted theorem Multiset.prod_ne_zero
deleted theorem Multiset.prod_nonneg
deleted theorem Multiset.single_le_prod
modified theorem Multiset.dvd_prod
added theorem Multiset.dvd_sum
added theorem Multiset.prod_eq_zero
added theorem Multiset.prod_map_neg
added theorem Multiset.prod_ne_zero
added theorem Multiset.prod_lt_prod'
added theorem Multiset.prod_nonneg
modified theorem Multiset.mem_product
modified theorem Multiset.mem_sigma
added theorem Multiset.nodup_bind
deleted theorem Multiset.dedup_bind_dedup
deleted theorem Multiset.nodup_bind